feat: elements of adjoin S are fixed by m iff elements of S are (leanprover-community#33989)

This PR proves:
```lean
(∀ x ∈ adjoin F S, m • x = x) ↔ (∀ x ∈ S, m • x = x)
```
both in the `Algebra.adjoin` and `IntermediateField.adjoin` cases

Author: xroblot

Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean

@@ -819,6 +819,11 @@ theorem ext_of_eq_adjoin {S : Subalgebra R A} {s : Set A} (hS : S = adjoin R s)
     φ₁ = φ₂ := by
   subst hS; exact adjoin_ext h
 
+theorem _root_.Algebra.forall_mem_adjoin_smul_eq_self_iff (S : Set A) {M : Type*} [Monoid M]
+    [MulSemiringAction M A] [SMulCommClass M R A] (m : M) :
+    (∀ x ∈ adjoin R S, m • x = x) ↔ (∀ x ∈ S, m • x = x) :=
+  AlgHom.eqOn_adjoin_iff (φ := MulSemiringAction.toAlgHom R A m) (ψ := .id R A)
+
 end AlgHom
 
 section NatInt

Mathlib/FieldTheory/Fixed.lean

@@ -42,9 +42,9 @@ universe u v w
 
 variable {M : Type u} [Monoid M]
 variable (G : Type u) [Group G]
-variable (F : Type v) [Field F] [MulSemiringAction M F] [MulSemiringAction G F] (m : M)
+variable (K : Type*) (F : Type v) [Field F] [MulSemiringAction M F] [MulSemiringAction G F] (m : M)
 
-/-- The subfield of F fixed by the field endomorphism `m`. -/
+/-- The subfield of `F` fixed by the field endomorphism `m`. -/
 def FixedBy.subfield : Subfield F where
   carrier := fixedBy F m
   zero_mem' := smul_zero m
@@ -54,6 +54,21 @@ def FixedBy.subfield : Subfield F where
   mul_mem' hx hy := (smul_mul' m _ _).trans <| congr_arg₂ _ hx hy
   inv_mem' x hx := (smul_inv'' m x).trans <| congr_arg _ hx
 
+@[simp]
+theorem FixedBy.subfield_mem_iff (x : F) :
+    x ∈ FixedBy.subfield F m ↔ m • x = x := Iff.rfl
+
+variable [Field K] [Algebra K F] [SMulCommClass M K F]
+
+/-- The intermediate field between `K` and `F` fixed by the field endomorphism `m`. -/
+def FixedBy.intermediateField : IntermediateField K F where
+  __ := FixedBy.subfield F m
+  algebraMap_mem' x := smul_algebraMap m x
+
+@[simp]
+theorem FixedBy.intermediateField_mem_iff (x : F) :
+    x ∈ FixedBy.intermediateField K F m ↔ m • x = x := Iff.rfl
+
 section InvariantSubfields
 
 variable (M) {F}

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

@@ -7,9 +7,8 @@ module
 
 public import Mathlib.Algebra.Algebra.Subalgebra.Directed
 public import Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
-public import Mathlib.FieldTheory.Separable
+public import Mathlib.FieldTheory.Fixed
 public import Mathlib.FieldTheory.SplittingField.IsSplittingField
-public import Mathlib.LinearAlgebra.Dual.Lemmas
 public import Mathlib.RingTheory.Adjoin.Dimension
 public import Mathlib.RingTheory.TensorProduct.Finite
 
@@ -63,6 +62,12 @@ theorem mem_adjoin_simple_iff {α : E} (x : E) :
   simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval,
     AlgHom.mem_range, exists_exists_eq_and]
 
+theorem forall_mem_adjoin_smul_eq_self_iff {M : Type*} [Monoid M] [MulSemiringAction M E]
+    [SMulCommClass M F E] (m : M) :
+    (∀ x ∈ adjoin F S, m • x = x) ↔ ∀ x ∈ S, m • x = x := by
+  change adjoin F S ≤ FixedBy.intermediateField F E m ↔ _
+  simp [IntermediateField.adjoin_le_iff, Set.subset_def]
+
 variable {F}
 
 section Supremum