Minimize Mathlib imports

[mpenciak]

This PR minimizes the usage of import Mathlib and replaces it with more targeted Mathlib imports

I noticed some slow compilation issues (likely related to this Zulip thread) while I was going through and first getting familiar with the library structure, and this fixes it to a certain extent.

Some downsides of this:

• There are some unexpected outcomes in downstream files when one takes away import Mathlib
• Certain typeclass instance/coercions were unexpectedly being used in certain places
  • One in particular was OfNat ((Fp p) × Unit) 5 which went through deducing CommRing Unit in
    Lampe.Builtin.Struct was a surprising one.

The only occurence of import Mathlib that remains is in Lampe.lean which has a bunch of examples. That rely on aesop to function. Perhaps these examples could be moved to a separate example file, and Lampe.lean could be the root of the library for end-users to import?