diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean
index 60959d38776780..d1fbd9298e67b3 100644
--- a/Mathlib/FieldTheory/AbelRuffini.lean
+++ b/Mathlib/FieldTheory/AbelRuffini.lean
@@ -25,7 +25,7 @@ that is solvable by radicals has a solvable Galois group.
 
 noncomputable section
 
-open Polynomial IntermediateField
+open Polynomial
 
 section AbelRuffini
 
@@ -295,6 +295,8 @@ theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (
       rw [sub_comp, X_comp, C_comp]
       exact gal_X_pow_sub_C_isSolvable n q
 
+open IntermediateField
+
 /-- An auxiliary induction lemma, which is generalized by `solvableByRad.isSolvable`. -/
 theorem induction2 {α β γ : solvableByRad F E} (hγ : γ ∈ F⟮α, β⟯) (hα : P α) (hβ : P β) : P γ := by
   let p := minpoly F α
diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean
index 3122aa50c36ee9..9acf5927e3f9be 100644
--- a/Mathlib/FieldTheory/Galois/Basic.lean
+++ b/Mathlib/FieldTheory/Galois/Basic.lean
@@ -186,32 +186,61 @@ def FixedPoints.intermediateField (M : Type*) [Monoid M] [MulSemiringAction M E]
 
 namespace IntermediateField
 
-/-- The intermediate field fixed by a subgroup -/
+/-- The intermediate field fixed by a subgroup. -/
 def fixedField : IntermediateField F E :=
   FixedPoints.intermediateField H
 
-theorem mem_fixedField_iff (x) :
+@[simp] lemma mem_fixedField_iff (x) :
     x ∈ fixedField H ↔ ∀ f ∈ H, f x = x := by
   show x ∈ MulAction.fixedPoints H E ↔ _
   simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]
 
+@[simp] lemma fixedField_bot : fixedField (⊥ : Subgroup (E ≃ₐ[F] E)) = ⊤ := by
+  ext
+  simp
+
 theorem finrank_fixedField_eq_card [FiniteDimensional F E] [DecidablePred (· ∈ H)] :
     finrank (fixedField H) E = Fintype.card H :=
   FixedPoints.finrank_eq_card H E
 
-/-- The subgroup fixing an intermediate field -/
+/-- The subgroup fixing an intermediate field. -/
 nonrec def fixingSubgroup : Subgroup (E ≃ₐ[F] E) :=
   fixingSubgroup (E ≃ₐ[F] E) (K : Set E)
 
 theorem le_iff_le : K ≤ fixedField H ↔ H ≤ fixingSubgroup K :=
   ⟨fun h g hg x => h (Subtype.mem x) ⟨g, hg⟩, fun h x hx g => h (Subtype.mem g) ⟨x, hx⟩⟩
 
-lemma fixingSubgroup_anti : Antitone (IntermediateField.fixingSubgroup (F := F) (E := E)) := by
-  intro K K' h
-  rw [← le_iff_le]
-  exact le_trans h ((le_iff_le _ _).mpr (le_refl K'.fixingSubgroup))
+/-- The map `K ↦ Gal(E/K)` is inclusion-reversing. -/
+theorem fixingSubgroup_le {K1 K2 : IntermediateField F E} (h12 : K1 ≤ K2) :
+    K2.fixingSubgroup ≤ K1.fixingSubgroup :=
+  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩
+
+@[deprecated (since := "2025-05-02")] alias fixingSubgroup.antimono := fixingSubgroup_le
+
+theorem fixedField_le {H1 H2 : Subgroup (E ≃ₐ[F] E)} (h12 : H1 ≤ H2) :
+    fixedField H2 ≤ fixedField H1 :=
+  fun _ hσ ⟨x, hx⟩ ↦ hσ ⟨x, h12 hx⟩
+
+lemma fixingSubgroup_antitone : Antitone (@fixingSubgroup F _ E _ _) :=
+  fun _ _ ↦ fixingSubgroup_le
+
+@[deprecated (since := "2025-05-02")] alias fixingSubgroup_anti := fixingSubgroup_antitone
+
+lemma fixedField_antitone : Antitone (@fixedField F _ E _ _) :=
+  fun _ _ ↦ fixedField_le
 
-/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `E ≃ₐ[K] E` -/
+@[simp] lemma mem_fixingSubgroup_iff (σ) : σ ∈ fixingSubgroup K ↔ ∀ x ∈ K, σ x = x :=
+  _root_.mem_fixingSubgroup_iff _
+
+@[simp] lemma fixingSubgroup_top : fixingSubgroup (⊤ : IntermediateField F E) = ⊥ := by
+  ext
+  simp [DFunLike.ext_iff]
+
+@[simp] lemma fixingSubgroup_bot : fixingSubgroup (⊥ : IntermediateField F E) = ⊤ := by
+  ext
+  simp [mem_bot]
+
+/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `E ≃ₐ[K] E`. -/
 def fixingSubgroupEquiv : fixingSubgroup K ≃* E ≃ₐ[K] E where
   toFun ϕ := { AlgEquiv.toRingEquiv (ϕ : E ≃ₐ[F] E) with commutes' := ϕ.mem }
   invFun ϕ := ⟨ϕ.restrictScalars _, ϕ.commutes⟩
@@ -264,6 +293,19 @@ theorem fixedField_fixingSubgroup [FiniteDimensional F E] [h : IsGalois F E] :
     Fintype.card_congr (IntermediateField.fixingSubgroupEquiv K).toEquiv]
   exact (card_aut_eq_finrank K E).symm
 
+@[simp] lemma fixedField_top [IsGalois F E] [FiniteDimensional F E] :
+    fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥ := by
+  rw [← fixingSubgroup_bot, fixedField_fixingSubgroup]
+
+theorem mem_bot_iff_fixed [IsGalois F E] [FiniteDimensional F E] (x : E) :
+    x ∈ (⊥ : IntermediateField F E) ↔ ∀ f : E ≃ₐ[F] E, f x = x := by
+  rw [← fixedField_top, mem_fixedField_iff]
+  simp only [Subgroup.mem_top, forall_const]
+
+theorem mem_range_algebraMap_iff_fixed [IsGalois F E] [FiniteDimensional F E] (x : E) :
+    x ∈ Set.range (algebraMap F E) ↔ ∀ f : E ≃ₐ[F] E, f x = x :=
+  mem_bot_iff_fixed x
+
 theorem card_fixingSubgroup_eq_finrank [DecidablePred (· ∈ IntermediateField.fixingSubgroup K)]
     [FiniteDimensional F E] [IsGalois F E] :
     Fintype.card (IntermediateField.fixingSubgroup K) = finrank K E := by
@@ -281,7 +323,7 @@ def intermediateFieldEquivSubgroup [FiniteDimensional F E] [IsGalois F E] :
     rw [← fixedField_fixingSubgroup L, IntermediateField.le_iff_le, fixedField_fixingSubgroup L]
     rfl
 
-/-- The Galois correspondence as a `GaloisInsertion` -/
+/-- The Galois correspondence as a `GaloisInsertion`. -/
 def galoisInsertionIntermediateFieldSubgroup [FiniteDimensional F E] :
     GaloisInsertion (OrderDual.toDual ∘
       (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
@@ -292,7 +334,7 @@ def galoisInsertionIntermediateFieldSubgroup [FiniteDimensional F E] :
   le_l_u H := le_of_eq (IntermediateField.fixingSubgroup_fixedField H).symm
   choice_eq _ _ := rfl
 
-/-- The Galois correspondence as a `GaloisCoinsertion` -/
+/-- The Galois correspondence as a `GaloisCoinsertion`. -/
 def galoisCoinsertionIntermediateFieldSubgroup [FiniteDimensional F E] [IsGalois F E] :
     GaloisCoinsertion (OrderDual.toDual ∘
       (IntermediateField.fixingSubgroup : IntermediateField F E → Subgroup (E ≃ₐ[F] E)))
@@ -315,8 +357,8 @@ open scoped Pointwise
 
 lemma IntermediateField.restrictNormalHom_ker (E : IntermediateField K L) [Normal K E] :
     (restrictNormalHom E).ker = E.fixingSubgroup := by
-  simp [fixingSubgroup, Subgroup.ext_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
-    restrictNormalHom_apply, mem_fixingSubgroup_iff]
+  simp only [Subgroup.ext_iff, MonoidHom.mem_ker, AlgEquiv.ext_iff, one_apply, Subtype.ext_iff,
+    restrictNormalHom_apply, Subtype.forall, mem_fixingSubgroup_iff, implies_true]
 
 namespace IsGalois
 
@@ -478,7 +520,7 @@ theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separ
   refine LinearEquiv.finrank_eq ?_
   rfl
 
-/-- Equivalent characterizations of a Galois extension of finite degree -/
+/-- Equivalent characterizations of a Galois extension of finite degree. -/
 theorem tfae [FiniteDimensional F E] : List.TFAE [
     IsGalois F E,
     IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E)) = ⊥,
diff --git a/Mathlib/FieldTheory/Galois/Infinite.lean b/Mathlib/FieldTheory/Galois/Infinite.lean
index ac53f58a56c098..60adf14e38e647 100644
--- a/Mathlib/FieldTheory/Galois/Infinite.lean
+++ b/Mathlib/FieldTheory/Galois/Infinite.lean
@@ -150,7 +150,7 @@ lemma fixingSubgroup_fixedField (H : ClosedSubgroup (K ≃ₐ[k] K)) [IsGalois k
     apply sub'
     simp only [← muleq, ← eq]
     apply Set.smul_mem_smul_set
-    exact (IntermediateField.fixingSubgroup.antimono (IntermediateField.le_normalClosure L) hτ)
+    exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)
   have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x :=
     fun x hx ↦ ((mem_fixingSubgroup_iff (K ≃ₐ[k] K)).mp hσ) x hx.1
   rw [restrict_fixedField H.1 L'.1] at fix
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
index 1d8612a920034e..033e0b0073a739 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
@@ -188,25 +188,6 @@ theorem iSup_toSubfield {ι : Sort*} [Nonempty ι] (S : ι → IntermediateField
     (iSup S).toSubfield = ⨆ i, (S i).toSubfield := by
   simp only [iSup, Set.range_nonempty, sSup_toSubfield, ← Set.range_comp, Function.comp_def]
 
-/-- Construct an algebra isomorphism from an equality of intermediate fields -/
-@[simps! apply]
-def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T :=
-  Subalgebra.equivOfEq _ _ (congr_arg toSubalgebra h)
-
-@[simp]
-theorem equivOfEq_symm {S T : IntermediateField F E} (h : S = T) :
-    (equivOfEq h).symm = equivOfEq h.symm :=
-  rfl
-
-@[simp]
-theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl := by
-  ext; rfl
-
-@[simp]
-theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
-    (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
-  rfl
-
 variable (F E)
 
 /-- The bottom intermediate_field is isomorphic to the field. -/
@@ -311,24 +292,6 @@ theorem _root_.AlgEquiv.fieldRange_eq_top (f : E ≃ₐ[F] K) :
 
 end Lattice
 
-section equivMap
-
-variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E]
-  {K : Type*} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K)
-
-theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f := toSubalgebra_injective <| by
-  rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
-
-/-- An intermediate field is isomorphic to its image under an `AlgHom`
-(which is automatically injective) -/
-noncomputable def equivMap : L ≃ₐ[F] L.map f :=
-  (AlgEquiv.ofInjective _ (f.comp L.val).injective).trans (equivOfEq (fieldRange_comp_val L f))
-
-@[simp]
-theorem coe_equivMap_apply (x : L) : ↑(equivMap L f x) = f x := rfl
-
-end equivMap
-
 section AdjoinDef
 
 variable (F : Type*) [Field F] {E : Type*} [Field E] [Algebra F E] (S : Set E)
diff --git a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean
index f134a4e0b15cd0..0017b353da7cd9 100644
--- a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean
@@ -97,6 +97,15 @@ theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E)
     (h_finrank : finrank F L = finrank E L) : F = E :=
   eq_of_le_of_finrank_le' h_le h_finrank.le
 
+/-- Mapping a finite dimensional intermediate field along an algebra equivalence gives
+a finite-dimensional intermediate field. -/
+instance finiteDimensional_map (f : L →ₐ[K] L) [FiniteDimensional K E] :
+    FiniteDimensional K (E.map f) :=
+  LinearEquiv.finiteDimensional (IntermediateField.equivMap E f).toLinearEquiv
+
+@[deprecated (since := "2025-05-02")]
+alias _root_.im_finiteDimensional := IntermediateField.finiteDimensional_map
+
 end FiniteDimensional
 
 theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
diff --git a/Mathlib/FieldTheory/IntermediateField/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Basic.lean
index e7b60e98f30607..d83abcca065ace 100644
--- a/Mathlib/FieldTheory/IntermediateField/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Basic.lean
@@ -163,7 +163,7 @@ protected theorem mul_mem {x y : L} : x ∈ S → y ∈ S → x * y ∈ S :=
 protected theorem add_mem {x y : L} : x ∈ S → y ∈ S → x + y ∈ S :=
   add_mem
 
-/-- An intermediate field is closed under subtraction -/
+/-- An intermediate field is closed under subtraction. -/
 protected theorem sub_mem {x y : L} : x ∈ S → y ∈ S → x - y ∈ S :=
   sub_mem
 
@@ -242,7 +242,7 @@ instance instSMulMemClass : SMulMemClass (IntermediateField K L) K L where
 
 end IntermediateField
 
-/-- Turn a subalgebra closed under inverses into an intermediate field -/
+/-- Turn a subalgebra closed under inverses into an intermediate field. -/
 def Subalgebra.toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
     IntermediateField K L :=
   { S with
@@ -260,7 +260,7 @@ theorem toIntermediateField_toSubalgebra (S : IntermediateField K L) :
   ext
   rfl
 
-/-- Turn a subalgebra satisfying `IsField` into an intermediate_field -/
+/-- Turn a subalgebra satisfying `IsField` into an intermediate_field. -/
 def Subalgebra.toIntermediateField' (S : Subalgebra K L) (hS : IsField S) : IntermediateField K L :=
   S.toIntermediateField fun x hx => by
     by_cases hx0 : x = 0
@@ -283,7 +283,7 @@ theorem toIntermediateField'_toSubalgebra (S : IntermediateField K L) :
   ext
   rfl
 
-/-- Turn a subfield of `L` containing the image of `K` into an intermediate field -/
+/-- Turn a subfield of `L` containing the image of `K` into an intermediate field. -/
 def Subfield.toIntermediateField (S : Subfield L) (algebra_map_mem : ∀ x, algebraMap K L x ∈ S) :
     IntermediateField K L :=
   { S with
@@ -291,7 +291,7 @@ def Subfield.toIntermediateField (S : Subfield L) (algebra_map_mem : ∀ x, alge
 
 namespace IntermediateField
 
-/-- An intermediate field inherits a field structure -/
+/-- An intermediate field inherits a field structure. -/
 instance toField : Field S :=
   S.toSubfield.toField
 
@@ -404,7 +404,7 @@ instance isScalarTower_mid {R : Type*} [Semiring R] [Algebra L R] [Algebra K R]
     [IsScalarTower K L R] : IsScalarTower K S R :=
   IsScalarTower.subalgebra' _ _ _ S.toSubalgebra
 
-/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L` -/
+/-- Specialize `is_scalar_tower_mid` to the common case where the top field is `L`. -/
 instance isScalarTower_mid' : IsScalarTower K S L :=
   inferInstance
 
@@ -444,6 +444,10 @@ theorem toSubalgebra_map (f : L →ₐ[K] L') : (S.map f).toSubalgebra = S.toSub
 theorem toSubfield_map (f : L →ₐ[K] L') : (S.map f).toSubfield = S.toSubfield.map f :=
   rfl
 
+/-- Mapping intermediate fields along the identity does not change them. -/
+theorem map_id : S.map (AlgHom.id K L) = S :=
+  SetLike.coe_injective <| Set.image_id _
+
 theorem map_map {K L₁ L₂ L₃ : Type*} [Field K] [Field L₁] [Algebra K L₁] [Field L₂] [Algebra K L₂]
     [Field L₃] [Algebra K L₃] (E : IntermediateField K L₁) (f : L₁ →ₐ[K] L₂) (g : L₂ →ₐ[K] L₃) :
     (E.map f).map g = E.map (g.comp f) :=
@@ -463,7 +467,7 @@ theorem gc_map_comap (f : L →ₐ[K] L') : GaloisConnection (map f) (comap f) :
 
 /-- Given an equivalence `e : L ≃ₐ[K] L'` of `K`-field extensions and an intermediate
 field `E` of `L/K`, `intermediateFieldMap e E` is the induced equivalence
-between `E` and `E.map e` -/
+between `E` and `E.map e`. -/
 def intermediateFieldMap (e : L ≃ₐ[K] L') (E : IntermediateField K L) : E ≃ₐ[K] E.map e.toAlgHom :=
   e.subalgebraMap E.toSubalgebra
 
@@ -603,7 +607,7 @@ variable {S}
 
 section Tower
 
-/-- Lift an intermediate_field of an intermediate_field -/
+/-- Lift an intermediate_field of an intermediate_field. -/
 def lift {F : IntermediateField K L} (E : IntermediateField K F) : IntermediateField K L :=
   E.map (val F)
 
@@ -618,7 +622,7 @@ theorem mem_lift {F : IntermediateField K L} {E : IntermediateField K F} (x : F)
     x.1 ∈ lift E ↔ x ∈ E :=
   Subtype.val_injective.mem_set_image
 
-/-- The algEquiv between an intermediate field and its lift -/
+/-- The algEquiv between an intermediate field and its lift. -/
 def liftAlgEquiv {E : IntermediateField K L} (F : IntermediateField K E) : ↥F ≃ₐ[K] lift F where
   toFun x := ⟨x.1.1, (mem_lift x.1).mpr x.2⟩
   invFun x := ⟨⟨x.1, lift_le F x.2⟩, (mem_lift ⟨x.1, lift_le F x.2⟩).mp x.2⟩
@@ -673,6 +677,43 @@ example {F : IntermediateField K L} {E : IntermediateField F L} : Algebra K E :=
 
 end Tower
 
+section equivMap
+
+variable {F : Type*} [Field F] {E : Type*} [Field E] [Algebra F E]
+  {K : Type*} [Field K] [Algebra F K] (L : IntermediateField F E) (f : E →ₐ[F] K)
+
+/-- Construct an algebra isomorphism from an equality of intermediate fields. -/
+@[simps! apply]
+def equivOfEq {S T : IntermediateField F E} (h : S = T) : S ≃ₐ[F] T :=
+  Subalgebra.equivOfEq _ _ (congr_arg toSubalgebra h)
+
+@[simp]
+theorem equivOfEq_symm {S T : IntermediateField F E} (h : S = T) :
+    (equivOfEq h).symm = equivOfEq h.symm :=
+  rfl
+
+@[simp]
+theorem equivOfEq_rfl (S : IntermediateField F E) : equivOfEq (rfl : S = S) = AlgEquiv.refl :=
+  AlgEquiv.ext fun _ ↦ rfl
+
+@[simp]
+theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T = U) :
+    (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
+  rfl
+
+theorem fieldRange_comp_val : (f.comp L.val).fieldRange = L.map f := toSubalgebra_injective <| by
+  rw [toSubalgebra_map, AlgHom.fieldRange_toSubalgebra, AlgHom.range_comp, range_val]
+
+/-- An intermediate field is isomorphic to its image under an `AlgHom`
+(which is automatically injective). -/
+noncomputable def equivMap : L ≃ₐ[F] L.map f :=
+  (AlgEquiv.ofInjective _ (f.comp L.val).injective).trans (equivOfEq (fieldRange_comp_val L f))
+
+@[simp]
+theorem coe_equivMap_apply (x : L) : ↑(equivMap L f x) = f x := rfl
+
+end equivMap
+
 end IntermediateField
 
 section ExtendScalars
diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index d5f2039fbd8a45..a2a8040645271a 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -6,7 +6,6 @@ Authors: Sebastian Monnet
 import Mathlib.FieldTheory.Galois.Basic
 import Mathlib.Topology.Algebra.FilterBasis
 import Mathlib.Topology.Algebra.OpenSubgroup
-import Mathlib.Tactic.ByContra
 
 /-!
 # Krull topology
@@ -58,80 +57,42 @@ all intermediate fields `E` with `E/K` finite dimensional.
 
 open scoped Pointwise
 
-/-- Mapping intermediate fields along the identity does not change them -/
-theorem IntermediateField.map_id {K L : Type*} [Field K] [Field L] [Algebra K L]
-    (E : IntermediateField K L) : E.map (AlgHom.id K L) = E :=
-  SetLike.coe_injective <| Set.image_id _
-
-/-- Mapping a finite dimensional intermediate field along an algebra equivalence gives
-a finite-dimensional intermediate field. -/
-instance im_finiteDimensional {K L : Type*} [Field K] [Field L] [Algebra K L]
-    {E : IntermediateField K L} (σ : L ≃ₐ[K] L) [FiniteDimensional K E] :
-    FiniteDimensional K (E.map σ.toAlgHom) :=
-  LinearEquiv.finiteDimensional (IntermediateField.intermediateFieldMap σ E).toLinearEquiv
-
 /-- Given a field extension `L/K`, `finiteExts K L` is the set of
-intermediate field extensions `L/E/K` such that `E/K` is finite -/
+intermediate field extensions `L/E/K` such that `E/K` is finite. -/
 def finiteExts (K : Type*) [Field K] (L : Type*) [Field L] [Algebra K L] :
     Set (IntermediateField K L) :=
   {E | FiniteDimensional K E}
 
 /-- Given a field extension `L/K`, `fixedByFinite K L` is the set of
-subsets `Gal(L/E)` of `L ≃ₐ[K] L`, where `E/K` is finite -/
+subsets `Gal(L/E)` of `L ≃ₐ[K] L`, where `E/K` is finite. -/
 def fixedByFinite (K L : Type*) [Field K] [Field L] [Algebra K L] : Set (Subgroup (L ≃ₐ[K] L)) :=
   IntermediateField.fixingSubgroup '' finiteExts K L
 
-/-- For a field extension `L/K`, the intermediate field `K` is finite-dimensional over `K` -/
-theorem IntermediateField.finiteDimensional_bot (K L : Type*) [Field K] [Field L] [Algebra K L] :
-    FiniteDimensional K (⊥ : IntermediateField K L) :=
-  .of_rank_eq_one IntermediateField.rank_bot
+@[deprecated (since := "2025-03-16")]
+alias IntermediateField.finiteDimensional_bot := IntermediateField.instFiniteSubtypeMemBot
 
-/-- This lemma says that `Gal(L/K) = L ≃ₐ[K] L` -/
-theorem IntermediateField.fixingSubgroup.bot {K L : Type*} [Field K] [Field L] [Algebra K L] :
-    IntermediateField.fixingSubgroup (⊥ : IntermediateField K L) = ⊤ := by
-  ext f
-  refine ⟨fun _ => Subgroup.mem_top _, fun _ => ?_⟩
-  rintro ⟨x, hx : x ∈ (⊥ : IntermediateField K L)⟩
-  rw [IntermediateField.mem_bot] at hx
-  rcases hx with ⟨y, rfl⟩
-  exact f.commutes y
+@[deprecated (since := "2025-03-12")]
+alias IntermediateField.fixingSubgroup.bot := IntermediateField.fixingSubgroup_bot
 
-/-- If `L/K` is a field extension, then we have `Gal(L/K) ∈ fixedByFinite K L` -/
+/-- If `L/K` is a field extension, then we have `Gal(L/K) ∈ fixedByFinite K L`. -/
 theorem top_fixedByFinite {K L : Type*} [Field K] [Field L] [Algebra K L] :
     ⊤ ∈ fixedByFinite K L :=
-  ⟨⊥, IntermediateField.finiteDimensional_bot K L, IntermediateField.fixingSubgroup.bot⟩
-
-/-- If `E1` and `E2` are finite-dimensional intermediate fields, then so is their compositum.
-This rephrases a result already in mathlib so that it is compatible with our type classes -/
-theorem finiteDimensional_sup {K L : Type*} [Field K] [Field L] [Algebra K L]
-    (E1 E2 : IntermediateField K L) (_ : FiniteDimensional K E1) (_ : FiniteDimensional K E2) :
-    FiniteDimensional K (↥(E1 ⊔ E2)) :=
-  IntermediateField.finiteDimensional_sup E1 E2
-
-/-- An element of `L ≃ₐ[K] L` is in `Gal(L/E)` if and only if it fixes every element of `E`. -/
-theorem IntermediateField.mem_fixingSubgroup_iff {K L : Type*} [Field K] [Field L] [Algebra K L]
-    (E : IntermediateField K L) (σ : L ≃ₐ[K] L) : σ ∈ E.fixingSubgroup ↔ ∀ x : L, x ∈ E → σ x = x :=
-  ⟨fun hσ x hx => hσ ⟨x, hx⟩, fun h ⟨x, hx⟩ => h x hx⟩
-
-/-- The map `E ↦ Gal(L/E)` is inclusion-reversing -/
-theorem IntermediateField.fixingSubgroup.antimono {K L : Type*} [Field K] [Field L] [Algebra K L]
-    {E1 E2 : IntermediateField K L} (h12 : E1 ≤ E2) : E2.fixingSubgroup ≤ E1.fixingSubgroup := by
-  rintro σ hσ ⟨x, hx⟩
-  exact hσ ⟨x, h12 hx⟩
+  ⟨⊥, IntermediateField.instFiniteSubtypeMemBot K, IntermediateField.fixingSubgroup_bot⟩
+
+@[deprecated (since := "2025-03-16")]
+alias finiteDimensional_sup := IntermediateField.finiteDimensional_sup
 
 /-- Given a field extension `L/K`, `galBasis K L` is the filter basis on `L ≃ₐ[K] L` whose sets
-are `Gal(L/E)` for intermediate fields `E` with `E/K` finite dimensional -/
+are `Gal(L/E)` for intermediate fields `E` with `E/K` finite dimensional. -/
 def galBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : FilterBasis (L ≃ₐ[K] L) where
   sets := (fun g => g.carrier) '' fixedByFinite K L
   nonempty := ⟨⊤, ⊤, top_fixedByFinite, rfl⟩
   inter_sets := by
-    rintro X Y ⟨H1, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨H2, ⟨E2, h_E2, rfl⟩, rfl⟩
-    use (IntermediateField.fixingSubgroup (E1 ⊔ E2)).carrier
-    refine ⟨⟨_, ⟨_, finiteDimensional_sup E1 E2 h_E1 h_E2, rfl⟩, rfl⟩, ?_⟩
-    rw [Set.subset_inter_iff]
-    exact
-      ⟨IntermediateField.fixingSubgroup.antimono le_sup_left,
-        IntermediateField.fixingSubgroup.antimono le_sup_right⟩
+    rintro _ _ ⟨_, ⟨E1, h_E1, rfl⟩, rfl⟩ ⟨_, ⟨E2, h_E2, rfl⟩, rfl⟩
+    have : FiniteDimensional K E1 := h_E1
+    have : FiniteDimensional K E2 := h_E2
+    refine ⟨(E1 ⊔ E2).fixingSubgroup.carrier, ⟨_, ⟨_, E1.finiteDimensional_sup E2, rfl⟩, rfl⟩, ?_⟩
+    exact Set.subset_inter (E1.fixingSubgroup_le le_sup_left) (E2.fixingSubgroup_le le_sup_right)
 
 /-- A subset of `L ≃ₐ[K] L` is a member of `galBasis K L` if and only if it is the underlying set
 of `Gal(L/E)` for some finite subextension `E/K`. -/
@@ -140,7 +101,7 @@ theorem mem_galBasis_iff (K L : Type*) [Field K] [Field L] [Algebra K L] (U : Se
   Iff.rfl
 
 /-- For a field extension `L/K`, `galGroupBasis K L` is the group filter basis on `L ≃ₐ[K] L`
-whose sets are `Gal(L/E)` for finite subextensions `E/K` -/
+whose sets are `Gal(L/E)` for finite subextensions `E/K`. -/
 def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] :
     GroupFilterBasis (L ≃ₐ[K] L) where
   toFilterBasis := galBasis K L
@@ -159,7 +120,7 @@ def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] :
     let F : IntermediateField K L := E.map σ.symm.toAlgHom
     refine ⟨F.fixingSubgroup.carrier, ⟨⟨F.fixingSubgroup, ⟨F, ?_, rfl⟩, rfl⟩, fun g hg => ?_⟩⟩
     · have : FiniteDimensional K E := hE
-      apply im_finiteDimensional σ.symm
+      exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom
     change σ * g * σ⁻¹ ∈ E.fixingSubgroup
     rw [IntermediateField.mem_fixingSubgroup_iff]
     intro x hx
@@ -173,7 +134,7 @@ def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] :
     exact AlgEquiv.apply_symm_apply σ x
 
 /-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
-`L ≃ₐ[K] L` induced by the group filter basis `galGroupBasis K L` -/
+`L ≃ₐ[K] L` induced by the group filter basis `galGroupBasis K L`. -/
 instance krullTopology (K L : Type*) [Field K] [Field L] [Algebra K L] :
     TopologicalSpace (L ≃ₐ[K] L) :=
   GroupFilterBasis.topology (galGroupBasis K L)
@@ -202,7 +163,7 @@ lemma krullTopology_mem_nhds_one_iff_of_normal (K L : Type*) [Field K] [Field L]
   refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩
   use (IntermediateField.normalClosure K E L)
   simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and]
-  exact le_trans (E.fixingSubgroup_anti E.le_normalClosure) hE
+  exact le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE
 
 section KrullT2
 
@@ -291,16 +252,6 @@ alias krullTopology_totallyDisconnected := krullTopology_isTotallySeparated
 
 end TotallySeparated
 
-@[simp] lemma IntermediateField.fixingSubgroup_top (K L : Type*) [Field K] [Field L] [Algebra K L] :
-    IntermediateField.fixingSubgroup (⊤ : IntermediateField K L) = ⊥ := by
-  ext
-  simp [mem_fixingSubgroup_iff, DFunLike.ext_iff]
-
-@[simp] lemma IntermediateField.fixingSubgroup_bot (K L : Type*) [Field K] [Field L] [Algebra K L] :
-    IntermediateField.fixingSubgroup (⊥ : IntermediateField K L) = ⊤ := by
-  ext
-  simp [mem_fixingSubgroup_iff, mem_bot]
-
 instance krullTopology_discreteTopology_of_finiteDimensional (K L : Type*) [Field K] [Field L]
     [Algebra K L] [FiniteDimensional K L] : DiscreteTopology (L ≃ₐ[K] L) := by
   rw [discreteTopology_iff_isOpen_singleton_one]
@@ -356,7 +307,7 @@ theorem finrank_eq_fixingSubgroup_index (L : IntermediateField k K) [IsGalois k
     let i := (liftAlgEquiv L').toLinearEquiv
     replace hfd := i.finiteDimensional
     rw [i.finrank_eq, this _ hfd] at hL'
-    exact (Subgroup.index_antitone <| fixingSubgroup.antimono <|
+    exact (Subgroup.index_antitone <| fixingSubgroup_le <|
       IntermediateField.lift_le L').not_lt hL'
   let E := normalClosure k L K
   have hle : L ≤ E := by simpa only [fieldRange_val] using L.val.fieldRange_le_normalClosure
diff --git a/Mathlib/FieldTheory/SeparableDegree.lean b/Mathlib/FieldTheory/SeparableDegree.lean
index 0de211d8a3b190..a5bf4540985e4c 100644
--- a/Mathlib/FieldTheory/SeparableDegree.lean
+++ b/Mathlib/FieldTheory/SeparableDegree.lean
@@ -900,7 +900,7 @@ if and only if every separable degree one polynomial splits. -/
 theorem perfectField_iff_splits_of_natSepDegree_eq_one (F : Type*) [Field F] :
     PerfectField F ↔ ∀ f : F[X], f.natSepDegree = 1 → f.Splits (RingHom.id F) := by
   refine ⟨fun ⟨h⟩ f hf ↦ or_iff_not_imp_left.2 fun hn g hg hd ↦ ?_, fun h ↦ ?_⟩
-  · rw [map_id] at hn hd
+  · rw [Polynomial.map_id] at hn hd
     have := natSepDegree_le_of_dvd g f hd hn
     rw [hf, (h hg).natSepDegree_eq_natDegree] at this
     exact (degree_eq_iff_natDegree_eq_of_pos one_pos).2 <| this.antisymm <|