dropping `import Mathbin` support

Stream: mathlib4

[Mario Carneiro]

mathport#187 implements defeq overrides, so alignments will by default occur even in the presence of type mismatches. This can cause downstream definitions to break, so it will stub things out as necessary, but this makes the resulting olean files more or less useless for users who are making use of the binport side: that is, downloading the nightlies as opaque versions of mathlib accessible via import Mathbin. In other words, there is a tension between making things usable for synport (i.e. taking the mathlib3port files and cleaning them up) and for binport (using mathlib as a black box in lean 4 via import Mathbin), and I think we should move to supporting the synport use case as porting gets under way.

It is still possible to enable the binport mode, but you have to do the build yourself since mathport will no longer be creating releases with binport support (or at least, if you import Mathbin be prepared to see a lot of proofs of Unit).