mathlib

7a21ae17 - chore(algebra/algebra/subalgebra): make inf and top definitionally convenient (#7812)

chore(algebra/algebra/subalgebra): make inf and top definitionally convenient (#7812) This adjusts the galois insertion such that `lemma coe_inf (S T : subalgebra R A) : (↑(S ⊓ T) : set A) = S ∩ T := rfl`. It also adds lots of trivial `simp` lemmas that were missing about the interactions of various coercions and lattice operations.