mathlib3

7c7195f6 - feat(field_theory/adjoin): lemmas about `inf`s of `intermediate_field`s (#10997)

feat(field_theory/adjoin): lemmas about `inf`s of `intermediate_field`s (#10997) This adjusts the data in the `galois_insertion` slightly such that this new lemma is true by `rfl`, to match how we handle this in `subalgebra`. As a result, `top_to_subalgebra` is now refl, but `adjoin_univ` is no longer refl. This also adds a handful of trivial simp lemmas.