mathlib3

ba60237b - chore(field_theory/adjoin): clarify and speed up proof (#14041)

chore(field_theory/adjoin): clarify and speed up proof (#14041) This PR turns a couple of refls into `simp` lemmas. Apart from being clearer now, this also speeds up the proof significantly in #11759 (where the elaborator chooses the wrong subexpression to unfold first). Elaboration time changed stayed about the same at about 300-350ms on master, and went from timeout to about 300ms on #11759.