mathlib3

3aac0287 - feat(field_theory/intermediate_field): equalities from inclusions and dimension bounds (#4828)