From 1316735627f7a0aedfe624e167618fc265cd1937 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 19:42:19 -0500
Subject: [PATCH 01/32] fix file mostly

---
 Mathlib/FieldTheory/KrullTopology.lean | 283 ++++++++++++++-----------
 1 file changed, 155 insertions(+), 128 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index ce539a76cba02d..76cc306a6cf5b8 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -7,7 +7,11 @@ module
 
 public import Mathlib.FieldTheory.Galois.Basic
 public import Mathlib.Topology.Algebra.FilterBasis
-public import Mathlib.Topology.Algebra.OpenSubgroup
+public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
+
+import Mathlib.Topology.Algebra.OpenSubgroup
+import Mathlib.Topology.Connected.Separation
+import Mathlib.Topology.UniformSpace.Separation
 
 /-!
 # Krull topology
@@ -60,103 +64,85 @@ all intermediate fields `E` with `E/K` finite dimensional.
 - `krullTopology K L` is defined as an instance for type class inference.
 -/
 
-@[expose] public section
-
-open scoped Pointwise
-
-/-- 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. -/
-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 `Gal(L/K)`, where `E/K` is finite. -/
-def fixedByFinite (K L : Type*) [Field K] [Field L] [Algebra K L] : Set (Subgroup Gal(L/K)) :=
-  IntermediateField.fixingSubgroup '' finiteExts 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.instFiniteSubtypeMemBot K, IntermediateField.fixingSubgroup_bot⟩
-
-/-- Given a field extension `L/K`, `galBasis K L` is the filter basis on `Gal(L/K)` whose sets
-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 Gal(L/K) where
-  sets := (fun g => g.carrier) '' fixedByFinite K L
-  nonempty := ⟨⊤, ⊤, top_fixedByFinite, rfl⟩
-  inter_sets := by
-    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)
+public section
 
-/-- A subset of `Gal(L/K)` 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`. -/
-theorem mem_galBasis_iff (K L : Type*) [Field K] [Field L] [Algebra K L] (U : Set Gal(L/K)) :
-    U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L :=
-  Iff.rfl
+open Filter
+open scoped Pointwise Uniformity
 
-/-- For a field extension `L/K`, `galGroupBasis K L` is the group filter basis on `Gal(L/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 Gal(L/K) where
-  toFilterBasis := galBasis K L
-  one' := fun ⟨H, _, h2⟩ => h2 ▸ H.one_mem
-  mul' {U} hU :=
-    ⟨U, hU, by
-      rcases hU with ⟨H, _, rfl⟩
-      rintro x ⟨a, haH, b, hbH, rfl⟩
-      exact H.mul_mem haH hbH⟩
-  inv' {U} hU :=
-    ⟨U, hU, by
-      rcases hU with ⟨H, _, rfl⟩
-      exact fun _ => H.inv_mem'⟩
-  conj' := by
-    rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩
-    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
-      exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom
-    change σ * g * σ⁻¹ ∈ E.fixingSubgroup
-    rw [IntermediateField.mem_fixingSubgroup_iff]
-    intro x hx
-    change σ (g (σ⁻¹ x)) = x
-    have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp⟩
-    have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x := by
-      rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
-      exact hg (σ⁻¹ x) h_in_F
-    rw [h_g_fix]
-    change σ (σ⁻¹ x) = x
-    exact AlgEquiv.apply_symm_apply σ x
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
 
+variable (K L) in
+@[no_expose]
+instance : UniformSpace Gal(L/K) := .ofCore
+  { uniformity := ⨅ (F : IntermediateField K L) (_ : FiniteDimensional K F),
+    𝓟 {p | Set.EqOn p.1 p.2 F}
+    refl := le_iInf₂ fun _ _ =>
+      principal_mono.2 (SetRel.id_subset_iff.2 ⟨fun _ => Set.eqOn_refl _ _⟩)
+    symm := tendsto_iInf_iInf fun _ => tendsto_iInf_iInf fun _ =>
+      Set.MapsTo.tendsto fun _ h => h.symm
+    comp := le_iInf₂ fun F hF =>
+      lift'_le (mem_iInf_of_mem F (mem_iInf_of_mem hF (mem_principal_self _)))
+        (principal_mono.2 (SetRel.isTrans_iff_comp_subset_self.1
+          ⟨fun _ _ _ h₁ h₂ => h₁.trans h₂⟩)) }
+
+open SetRel in
+theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} :
+    s ∈ 𝓤 Gal(L/K) ↔ ∃ F : IntermediateField K L,
+      FiniteDimensional K F ∧ ∀ σ τ : Gal(L/K), Set.EqOn σ τ F → σ ~[s] τ := by
+  let f : Set (IntermediateField K L) := {F | FiniteDimensional K F}
+  have hf : f.Nonempty := ⟨⊥, inferInstanceAs (FiniteDimensional K (⊥ : IntermediateField K L))⟩
+  refine (Filter.mem_biInf_of_directed ?_ hf).trans (by simp [Set.subset_def, Set.EqOn, f])
+  intro E hE F hF
+  simp only [Set.mem_setOf_eq, f] at hE hF ⊢
+  have hl : E ≤ E ⊔ F := le_sup_left
+  have hr : F ≤ E ⊔ F := le_sup_right
+  exact ⟨E ⊔ F, inferInstance,
+    principal_mono.2 fun p h x hx => h (hl hx),
+    principal_mono.2 fun p h x hx => h (hr hx)⟩
+
+variable (K L) in
 /-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
 `Gal(L/K)` induced by the group filter basis `galGroupBasis K L`. -/
 instance krullTopology (K L : Type*) [Field K] [Field L] [Algebra K L] :
-    TopologicalSpace Gal(L/K) :=
-  GroupFilterBasis.topology (galGroupBasis K L)
+    TopologicalSpace Gal(L/K) := inferInstance
 
+open IntermediateField in
+variable (K L) in
+set_option backward.isDefEq.respectTransparency false in
 /-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/
 @[stacks 0BMJ "We define Krull topology directly without proving the universal property"]
-instance (K L : Type*) [Field K] [Field L] [Algebra K L] : IsTopologicalGroup Gal(L/K) :=
-  GroupFilterBasis.isTopologicalGroup (galGroupBasis K L)
+instance : IsUniformGroup Gal(L/K) where
+  uniformContinuous_div s hs := by
+    rw [krullTopology_mem_uniformity_iff] at hs
+    obtain ⟨F, _, hF⟩ := hs
+    rw [uniformity_prod_eq_prod, map_map, mem_map, mem_prod_self_iff]
+    refine ⟨{p | Set.EqOn p.1 p.2 (normalClosure K F L)}, ?_, ?_⟩
+    · rw [krullTopology_mem_uniformity_iff]
+      exact ⟨_, inferInstance, fun _ _ h => h⟩
+    rw [Set.prod_subset_iff]
+    intro σ hσ τ hτ
+    simp only [Set.mem_preimage, Function.comp_apply]
+    refine hF _ _ fun x hx => ?_
+    simp only [div_eq_mul_inv, AlgEquiv.mul_apply, AlgEquiv.coe_inv]
+    have hn : τ.1.symm x ∈ normalClosure K F L := by
+      have h : (AlgHom.comp τ.1.symm (IsScalarTower.toAlgHom K F L)).fieldRange ≤
+          normalClosure K F L := AlgHom.fieldRange_le_normalClosure _
+      exact h (by simpa using hx)
+    rw [hσ hn, σ.2.injective.eq_iff, AlgEquiv.eq_symm_apply, ← hτ hn, τ.1.apply_symm_apply]
 
 open scoped Topology in
-lemma krullTopology_mem_nhds_one_iff (K L : Type*) [Field K] [Field L] [Algebra K L]
-    (s : Set Gal(L/K)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
+lemma krullTopology_mem_nhds_one_iff {s : Set Gal(L/K)} : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
     FiniteDimensional K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by
-  rw [GroupFilterBasis.nhds_one_eq]
-  constructor
-  · rintro ⟨-, ⟨-, ⟨E, fin, rfl⟩, rfl⟩, hE⟩
-    exact ⟨E, fin, hE⟩
-  · rintro ⟨E, fin, hE⟩
-    exact ⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩
+  rw [nhds_eq_comap_uniformity', ← le_principal_iff, comap_le_iff_le_kernMap,
+    kernMap_principal, le_principal_iff, krullTopology_mem_uniformity_iff]
+  refine exists_congr fun F => and_congr_right fun hF => ?_
+  rw [← Prod.forall', ← Set.setOf_subset, Set.subset_kernImage_iff]
+  exact Iff.of_eq congr($(by ext; simp [Set.EqOn]) ⊆ s)
 
 set_option backward.isDefEq.respectTransparency false in
 open scoped Topology in
-lemma krullTopology_mem_nhds_one_iff_of_normal (K L : Type*) [Field K] [Field L] [Algebra K L]
-    [Normal K L] (s : Set Gal(L/K)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
+lemma krullTopology_mem_nhds_one_iff_of_normal [Normal K L] {s : Set Gal(L/K)} :
+    s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
     FiniteDimensional K E ∧ Normal K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by
   rw [krullTopology_mem_nhds_one_iff]
   refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩
@@ -172,11 +158,8 @@ open scoped Topology Filter
   `Gal(L/K)`. -/
 theorem IntermediateField.fixingSubgroup_isOpen {K L : Type*} [Field K] [Field L] [Algebra K L]
     (E : IntermediateField K L) [FiniteDimensional K E] :
-    IsOpen (E.fixingSubgroup : Set Gal(L/K)) := by
-  have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L :=
-    ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩
-  have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
-  exact Subgroup.isOpen_of_mem_nhds _ h_nhds
+    IsOpen (E.fixingSubgroup : Set Gal(L/K)) :=
+  Subgroup.isOpen_of_mem_nhds _ (krullTopology_mem_nhds_one_iff.2 ⟨E, ‹_›, subset_rfl⟩)
 
 /-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ Gal(L/K)` is
   closed. -/
@@ -185,41 +168,6 @@ theorem IntermediateField.fixingSubgroup_isClosed {K L : Type*} [Field K] [Field
     IsClosed (E.fixingSubgroup : Set Gal(L/K)) :=
   OpenSubgroup.isClosed ⟨E.fixingSubgroup, E.fixingSubgroup_isOpen⟩
 
-/-- If `L/K` is an algebraic extension, then the Krull topology on `Gal(L/K)` is Hausdorff. -/
-theorem krullTopology_t2 {K L : Type*} [Field K] [Field L] [Algebra K L]
-    [Algebra.IsIntegral K L] : T2Space Gal(L/K) :=
-  { t2 := fun f g hfg => by
-      let φ := f⁻¹ * g
-      obtain ⟨x, hx⟩ := DFunLike.exists_ne hfg
-      have hφx : φ x ≠ x := by
-        apply ne_of_apply_ne f
-        change f (f.symm (g x)) ≠ f x
-        rw [AlgEquiv.apply_symm_apply f (g x), ne_comm]
-        exact hx
-      let E : IntermediateField K L := IntermediateField.adjoin K {x}
-      let h_findim : FiniteDimensional K E := IntermediateField.adjoin.finiteDimensional
-        (Algebra.IsIntegral.isIntegral x)
-      let H := E.fixingSubgroup
-      have h_basis : (H : Set Gal(L/K)) ∈ galGroupBasis K L := ⟨H, ⟨E, ⟨h_findim, rfl⟩⟩, rfl⟩
-      have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis
-      rw [mem_nhds_iff] at h_nhds
-      rcases h_nhds with ⟨W, hWH, hW_open, hW_1⟩
-      refine ⟨f • W, g • W,
-        ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, ?_⟩⟩
-      rw [Set.disjoint_left]
-      rintro σ ⟨w1, hw1, h⟩ ⟨w2, hw2, rfl⟩
-      dsimp at h
-      rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h
-      have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2))
-      rw [h] at h_in_H
-      change φ ∈ E.fixingSubgroup at h_in_H
-      rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H
-      specialize h_in_H x
-      have hxE : x ∈ E := by
-        apply IntermediateField.subset_adjoin
-        apply Set.mem_singleton
-      exact hφx (h_in_H hxE) }
-
 end KrullT2
 
 section TotallySeparated
@@ -240,8 +188,13 @@ instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L
     IntermediateField.mem_fixingSubgroup_iff, not_forall]
   exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
 
+/-- If `L/K` is an algebraic extension, then the Krull topology on `Gal(L/K)` is Hausdorff. -/
+instance krullTopology_t2 [Algebra.IsIntegral K L] : T2Space Gal(L/K) :=
+  TotallySeparatedSpace.t2Space
+
 /-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is
   totally separated. -/
+@[deprecated TotallySeparatedSpace.isTotallySeparated_univ (since := "2026-03-05")]
 theorem krullTopology_isTotallySeparated {K L : Type*} [Field K] [Field L] [Algebra K L]
     [Algebra.IsIntegral K L] : IsTotallySeparated (Set.univ : Set Gal(L/K)) :=
   (totallySeparatedSpace_iff _).mp inferInstance
@@ -249,11 +202,7 @@ theorem krullTopology_isTotallySeparated {K L : Type*} [Field K] [Field L] [Alge
 end TotallySeparated
 
 instance krullTopology_discreteTopology_of_finiteDimensional (K L : Type*) [Field K] [Field L]
-    [Algebra K L] [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := by
-  rw [discreteTopology_iff_isOpen_singleton_one]
-  change IsOpen ((⊥ : Subgroup Gal(L/K)) : Set Gal(L/K))
-  rw [← IntermediateField.fixingSubgroup_top]
-  exact IntermediateField.fixingSubgroup_isOpen ⊤
+    [Algebra K L] [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := inferInstance
 
 section MulAction
 
@@ -335,3 +284,81 @@ theorem finrank_eq_fixingSubgroup_index (L : IntermediateField k K) [IsGalois k
   exact lift_restrict hle
 
 end IntermediateField
+
+section deprecated
+set_option linter.deprecated false
+
+/-- 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. -/
+@[deprecated "deprecated without replacement" (since := "2026-03-05")]
+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 `Gal(L/K)`, where `E/K` is finite. -/
+@[deprecated "deprecated without replacement" (since := "2026-03-05")]
+def fixedByFinite (K L : Type*) [Field K] [Field L] [Algebra K L] : Set (Subgroup Gal(L/K)) :=
+  IntermediateField.fixingSubgroup '' finiteExts K L
+
+/-- If `L/K` is a field extension, then we have `Gal(L/K) ∈ fixedByFinite K L`. -/
+@[deprecated "deprecated without replacement" (since := "2026-03-05")]
+theorem top_fixedByFinite {K L : Type*} [Field K] [Field L] [Algebra K L] :
+    ⊤ ∈ fixedByFinite K L :=
+  ⟨⊥, IntermediateField.instFiniteSubtypeMemBot K, IntermediateField.fixingSubgroup_bot⟩
+
+/-- Given a field extension `L/K`, `galBasis K L` is the filter basis on `Gal(L/K)` whose sets
+are `Gal(L/E)` for intermediate fields `E` with `E/K` finite dimensional. -/
+@[deprecated "deprecated without replacement" (since := "2026-03-05")]
+def galBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : FilterBasis Gal(L/K) where
+  sets := (fun g => g.carrier) '' fixedByFinite K L
+  nonempty := ⟨⊤, ⊤, top_fixedByFinite, rfl⟩
+  inter_sets := by
+    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 `Gal(L/K)` 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`. -/
+@[deprecated "deprecated without replacement" (since := "2026-03-05")]
+theorem mem_galBasis_iff (K L : Type*) [Field K] [Field L] [Algebra K L] (U : Set Gal(L/K)) :
+    U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L :=
+  Iff.rfl
+
+/-- For a field extension `L/K`, `galGroupBasis K L` is the group filter basis on `Gal(L/K)`
+whose sets are `Gal(L/E)` for finite subextensions `E/K`. -/
+@[deprecated "deprecated without replacement" (since := "2026-03-05")]
+def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] :
+    GroupFilterBasis Gal(L/K) where
+  toFilterBasis := galBasis K L
+  one' := fun ⟨H, _, h2⟩ => h2 ▸ H.one_mem
+  mul' {U} hU :=
+    ⟨U, hU, by
+      rcases hU with ⟨H, _, rfl⟩
+      rintro x ⟨a, haH, b, hbH, rfl⟩
+      exact H.mul_mem haH hbH⟩
+  inv' {U} hU :=
+    ⟨U, hU, by
+      rcases hU with ⟨H, _, rfl⟩
+      exact fun _ => H.inv_mem'⟩
+  conj' := by
+    rintro σ U ⟨H, ⟨E, hE, rfl⟩, rfl⟩
+    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
+      exact IntermediateField.finiteDimensional_map σ.symm.toAlgHom
+    change σ * g * σ⁻¹ ∈ E.fixingSubgroup
+    rw [IntermediateField.mem_fixingSubgroup_iff]
+    intro x hx
+    change σ (g (σ⁻¹ x)) = x
+    have h_in_F : σ⁻¹ x ∈ F := ⟨x, hx, by dsimp⟩
+    have h_g_fix : g (σ⁻¹ x) = σ⁻¹ x := by
+      rw [Subgroup.mem_carrier, IntermediateField.mem_fixingSubgroup_iff F g] at hg
+      exact hg (σ⁻¹ x) h_in_F
+    rw [h_g_fix]
+    change σ (σ⁻¹ x) = x
+    exact AlgEquiv.apply_symm_apply σ x
+
+end deprecated

From 53e958f9632a6c5c20ac8897bd5c4082782ff51f Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 19:42:57 -0500
Subject: [PATCH 02/32] author

---
 Mathlib/FieldTheory/KrullTopology.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 76cc306a6cf5b8..69ebc27f65db90 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Sebastian Monnet. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Sebastian Monnet
+Authors: Sebastian Monnet, Aaron Liu
 -/
 module
 

From 9f359745b1038924db46444b87c623ef4f07c8e1 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 19:50:25 -0500
Subject: [PATCH 03/32] more work

---
 Mathlib/FieldTheory/KrullTopology.lean | 58 ++++++++++++++++----------
 1 file changed, 35 insertions(+), 23 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 69ebc27f65db90..27660723e661cb 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -103,8 +103,7 @@ theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} :
 variable (K L) in
 /-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
 `Gal(L/K)` induced by the group filter basis `galGroupBasis K L`. -/
-instance krullTopology (K L : Type*) [Field K] [Field L] [Algebra K L] :
-    TopologicalSpace Gal(L/K) := inferInstance
+instance krullTopology : TopologicalSpace Gal(L/K) := inferInstance
 
 open IntermediateField in
 variable (K L) in
@@ -154,26 +153,37 @@ section KrullT2
 
 open scoped Topology Filter
 
-/-- Let `L/E/K` be a tower of fields with `E/K` finite. Then `Gal(L/E)` is an open subgroup of
-  `Gal(L/K)`. -/
-theorem IntermediateField.fixingSubgroup_isOpen {K L : Type*} [Field K] [Field L] [Algebra K L]
-    (E : IntermediateField K L) [FiniteDimensional K E] :
-    IsOpen (E.fixingSubgroup : Set Gal(L/K)) :=
+/-- Let `L/E/K` be a tower of fields with `E/K` finite.
+Then `Gal(L/E)` is an open subgroup of `Gal(L/K)`. -/
+theorem IntermediateField.isOpen_fixingSubgroup (E : IntermediateField K L)
+    [FiniteDimensional K E] : IsOpen (E.fixingSubgroup : Set Gal(L/K)) :=
   Subgroup.isOpen_of_mem_nhds _ (krullTopology_mem_nhds_one_iff.2 ⟨E, ‹_›, subset_rfl⟩)
 
-/-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ Gal(L/K)` is
-  closed. -/
-theorem IntermediateField.fixingSubgroup_isClosed {K L : Type*} [Field K] [Field L] [Algebra K L]
-    (E : IntermediateField K L) [FiniteDimensional K E] :
-    IsClosed (E.fixingSubgroup : Set Gal(L/K)) :=
-  OpenSubgroup.isClosed ⟨E.fixingSubgroup, E.fixingSubgroup_isOpen⟩
+@[deprecated (since := "2026-03-05")]
+alias IntermediateField.fixingSubgroup_isOpen := IntermediateField.isOpen_fixingSubgroup
+
+/-- Given a tower of fields `L/E/K`, with `E/K` finite,
+the subgroup `Gal(L/E) ≤ Gal(L/K)` is closed. -/
+theorem IntermediateField.isClosed_fixingSubgroup (E : IntermediateField K L)
+    [Algebra.IsIntegral K E] : IsClosed (E.fixingSubgroup : Set Gal(L/K)) := by
+  have hx (x : E) : IsClosed ((adjoin K {(x : L)}).fixingSubgroup : Set Gal(L/K)) :=
+    have : FiniteDimensional K (adjoin K {(x : L)}) := IntermediateField.adjoin.finiteDimensional
+      (coe_isIntegral_iff.2 (Algebra.IsIntegral.isIntegral x))
+    Subgroup.isClosed_of_isOpen _ (isOpen_fixingSubgroup _)
+  convert isClosed_iInter hx
+  ext g
+  simp only [SetLike.mem_coe, mem_fixingSubgroup_iff, Set.mem_iInter, Subtype.forall]
+  exact ⟨fun h a ha x hx => h x (adjoin_simple_le_iff.2 ha hx),
+    fun h x hx => h x hx x (mem_adjoin_simple_self K x)⟩
+
+@[deprecated (since := "2026-03-05")]
+alias IntermediateField.fixingSubgroup_isClosed := IntermediateField.isClosed_fixingSubgroup
 
 end KrullT2
 
 section TotallySeparated
 
-instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :
-    TotallySeparatedSpace Gal(L/K) := by
+instance [Algebra.IsIntegral K L] : TotallySeparatedSpace Gal(L/K) := by
   rw [totallySeparatedSpace_iff_exists_isClopen]
   intro σ τ h_diff
   have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
@@ -182,7 +192,7 @@ instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L
   haveI := IntermediateField.adjoin.finiteDimensional
     (Algebra.IsIntegral.isIntegral (R := K) x)
   refine ⟨σ • E.fixingSubgroup,
-    ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩,
+    ⟨E.isClosed_fixingSubgroup.leftCoset σ, E.isOpen_fixingSubgroup.leftCoset σ⟩,
     ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩
   simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe,
     IntermediateField.mem_fixingSubgroup_iff, not_forall]
@@ -195,19 +205,18 @@ instance krullTopology_t2 [Algebra.IsIntegral K L] : T2Space Gal(L/K) :=
 /-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is
   totally separated. -/
 @[deprecated TotallySeparatedSpace.isTotallySeparated_univ (since := "2026-03-05")]
-theorem krullTopology_isTotallySeparated {K L : Type*} [Field K] [Field L] [Algebra K L]
-    [Algebra.IsIntegral K L] : IsTotallySeparated (Set.univ : Set Gal(L/K)) :=
+theorem krullTopology_isTotallySeparated [Algebra.IsIntegral K L] :
+    IsTotallySeparated (Set.univ : Set Gal(L/K)) :=
   (totallySeparatedSpace_iff _).mp inferInstance
 
 end TotallySeparated
 
-instance krullTopology_discreteTopology_of_finiteDimensional (K L : Type*) [Field K] [Field L]
-    [Algebra K L] [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := inferInstance
+variable (K L) in
+instance krullTopology_discreteTopology_of_finiteDimensional
+    [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := inferInstance
 
 section MulAction
 
-variable {K L : Type*} [Field K] [Field L] [Algebra K L]
-
 /-- If `L/K` is an algebraic field extension, then the stabilizer
 in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/
 theorem stabilizer_isOpen_of_isIntegral [Algebra.IsIntegral K L] (x : L) :
@@ -215,12 +224,15 @@ theorem stabilizer_isOpen_of_isIntegral [Algebra.IsIntegral K L] (x : L) :
   open IntermediateField in
   let E := adjoin K {x}
   have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
-  convert fixingSubgroup_isOpen E
+  convert isOpen_fixingSubgroup E
   ext g
   simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm
 
 end MulAction
 
+/- This next section doesn't seem to be about the krull topology,
+and is completely independent from the rest of the file
+(it still compiles if I delete everything else). -/
 namespace IntermediateField
 
 variable {k E : Type*} (K : Type*) [Field k] [Field E] [Field K]

From 8a9354e07ec6c3058520683527865df1ef53669f Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 21:25:49 -0500
Subject: [PATCH 04/32] fix one file

---
 Mathlib/FieldTheory/Galois/Infinite.lean | 28 ++++++++++--------------
 1 file changed, 11 insertions(+), 17 deletions(-)

diff --git a/Mathlib/FieldTheory/Galois/Infinite.lean b/Mathlib/FieldTheory/Galois/Infinite.lean
index 81eca59c3e99ae..132ad8027a8c76 100644
--- a/Mathlib/FieldTheory/Galois/Infinite.lean
+++ b/Mathlib/FieldTheory/Galois/Infinite.lean
@@ -76,7 +76,7 @@ lemma fixingSubgroup_isClosed (L : IntermediateField k K) [IsGalois k K] :
       have : g y = y := (mem_fixingSubgroup_iff Gal(K/k)).mp hg y <|
         adjoin_simple_le_iff.mp le_rfl
       simpa only [this, ne_eq, AlgEquiv.smul_def] using ne
-    · simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and]
+    · simp only [(IntermediateField.isOpen_fixingSubgroup (adjoin k {y}).1).smul σ, true_and]
       use 1
       simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]
 
@@ -151,21 +151,17 @@ lemma fixingSubgroup_fixedField (H : ClosedSubgroup Gal(K/k)) [IsGalois k K] :
   intro σ hσ
   by_contra h
   have nhds : H.carrierᶜ ∈ nhds σ := H.isClosed'.isOpen_compl.mem_nhds h
-  rw [GroupFilterBasis.nhds_eq (x₀ := σ) (galGroupBasis k K)] at nhds
-  rcases nhds with ⟨b, ⟨gp, ⟨L, hL, eq'⟩, eq⟩, sub⟩
-  rw [← eq'] at eq
-  have := hL.out
+  rw [← map_mul_left_nhds_one, Filter.mem_map, krullTopology_mem_nhds_one_iff] at nhds
+  rcases nhds with ⟨L, hL, sub⟩
   let L' : FiniteGaloisIntermediateField k K := {
     normalClosure k L K with
     finiteDimensional := normalClosure.is_finiteDimensional k L K
     isGalois := IsGalois.normalClosure k L K }
-  have compl : σ • L'.1.fixingSubgroup.carrier ⊆ H.carrierᶜ := by
-    rintro φ ⟨τ, hτ, muleq⟩
-    have sub' : σ • b ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr sub
-    apply sub'
-    simp only [← muleq, ← eq]
-    apply Set.smul_mem_smul_set
-    exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)
+  have compl : σ • L'.1.fixingSubgroup.carrier ⊆ H.carrierᶜ :=
+    calc σ • (SetLike.coe L'.1.fixingSubgroup)
+      _ ⊆ σ • (SetLike.coe L.fixingSubgroup) :=
+        Set.smul_set_mono (fixingSubgroup_antitone (L.le_normalClosure))
+      _ ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr sub
   have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x :=
     fun x hx ↦ ((mem_fixingSubgroup_iff Gal(K/k)).mp hσ) x hx.1
   rw [restrict_fixedField H.1 L'.1] at fix
@@ -243,13 +239,11 @@ set_option backward.isDefEq.respectTransparency false in
 open IntermediateField in
 theorem isOpen_iff_finite (L : IntermediateField k K) [IsGalois k K] :
     IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k L := by
-  refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.fixingSubgroup_isOpen L⟩
+  refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.isOpen_fixingSubgroup L⟩
   have : (IntermediateFieldEquivClosedSubgroup.toFun L).carrier ∈ nhds 1 :=
     IsOpen.mem_nhds h (congrFun rfl)
-  rw [GroupFilterBasis.nhds_one_eq] at this
-  rcases this with ⟨S, ⟨gp, ⟨M, hM, eq'⟩, eq⟩, sub⟩
-  rw [← eq, ← eq'] at sub
-  have := hM.out
+  rw [krullTopology_mem_nhds_one_iff] at this
+  rcases this with ⟨M, hM, sub⟩
   let L' : FiniteGaloisIntermediateField k K := {
     normalClosure k M K with
     finiteDimensional := normalClosure.is_finiteDimensional k M K

From 359fa28c940df11909001265743079ba520f4f9b Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 21:37:17 -0500
Subject: [PATCH 05/32] fix the other file

---
 .../Cyclotomic/CyclotomicCharacter.lean            | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
index cd69509024e11b..1056a5509e8e7a 100644
--- a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
@@ -343,23 +343,23 @@ lemma cyclotomicCharacter.continuous (p : ℕ) [Fact p.Prime]
   choose ζ hζ using H
   refine Continuous.of_coeHom_comp ?_
   apply continuous_of_continuousAt_one
-  rw [ContinuousAt, map_one, (galGroupBasis K L).nhds_one_hasBasis.tendsto_iff
-    (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))]
+  rw [Metric.continuousAt_iff']
   intro ε hε
+  rw [Filter.eventually_iff, krullTopology_mem_nhds_one_iff]
   obtain ⟨k, hk', hk⟩ : ∃ k : ℕ, k ≠ 0 ∧ p ^ (-k : ℤ) < ε := by
     obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε
     exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩
-  refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩
+  refine ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, ?_⟩
   · exact ((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top
   · intro σ hσ
     refine lt_of_le_of_lt ?_ hk
     dsimp
     rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow,
-      RingHom.mem_ker, map_sub, map_one, cyclotomicCharacter.toZModPow,
+      RingHom.mem_ker, map_sub, cyclotomicCharacter.toZModPow,
       sub_eq_zero, eq_comm]
     apply modularCyclotomicCharacter.unique
     intro t ht
     obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht
-    rw [ZMod.val_one'', pow_one]
-    · exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩
-    · exact (one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne'
+    rw [show ((1 : Gal(L/K)) : L ≃+* L) = 1 from rfl, map_one, Units.val_one, map_one,
+      ZMod.val_one'' (one_lt_pow₀ (Nat.Prime.one_lt Fact.out) hk').ne', pow_one]
+    exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩

From d65ea4788738e933c4453a4b9710df85d781b4d0 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 21:49:00 -0500
Subject: [PATCH 06/32] Update Mathlib/FieldTheory/KrullTopology.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
---
 Mathlib/FieldTheory/KrullTopology.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 27660723e661cb..db9c62dc715279 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -109,7 +109,7 @@ open IntermediateField in
 variable (K L) in
 set_option backward.isDefEq.respectTransparency false in
 /-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/
-@[stacks 0BMJ "We define Krull topology directly without proving the universal property"]
+@[stacks 0BMJ "We define the Krull topology directly without proving the universal property"]
 instance : IsUniformGroup Gal(L/K) where
   uniformContinuous_div s hs := by
     rw [krullTopology_mem_uniformity_iff] at hs

From 33711bfa223057c394473912a8459dcddb27d57f Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 21:49:18 -0500
Subject: [PATCH 07/32] Update Mathlib/FieldTheory/KrullTopology.lean
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>
---
 Mathlib/FieldTheory/KrullTopology.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index db9c62dc715279..645dc1f6a2b635 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -75,7 +75,7 @@ variable (K L) in
 @[no_expose]
 instance : UniformSpace Gal(L/K) := .ofCore
   { uniformity := ⨅ (F : IntermediateField K L) (_ : FiniteDimensional K F),
-    𝓟 {p | Set.EqOn p.1 p.2 F}
+      𝓟 {p | Set.EqOn p.1 p.2 F}
     refl := le_iInf₂ fun _ _ =>
       principal_mono.2 (SetRel.id_subset_iff.2 ⟨fun _ => Set.eqOn_refl _ _⟩)
     symm := tendsto_iInf_iInf fun _ => tendsto_iInf_iInf fun _ =>

From cbf6271fe6045961ab9eaf8505a5c3fdac31bafe Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 21:53:47 -0500
Subject: [PATCH 08/32] little reshuffling of rewrites

---
 Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
index 1056a5509e8e7a..a1a4a2c6482d3e 100644
--- a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
@@ -355,11 +355,10 @@ lemma cyclotomicCharacter.continuous (p : ℕ) [Fact p.Prime]
     refine lt_of_le_of_lt ?_ hk
     dsimp
     rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow,
-      RingHom.mem_ker, map_sub, cyclotomicCharacter.toZModPow,
-      sub_eq_zero, eq_comm]
+      RingHom.mem_ker, show ((1 : Gal(L/K)) : L ≃+* L) = 1 from rfl, map_one,
+      map_sub, cyclotomicCharacter.toZModPow, sub_eq_zero, eq_comm, Units.val_one, map_one]
     apply modularCyclotomicCharacter.unique
     intro t ht
     obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht
-    rw [show ((1 : Gal(L/K)) : L ≃+* L) = 1 from rfl, map_one, Units.val_one, map_one,
-      ZMod.val_one'' (one_lt_pow₀ (Nat.Prime.one_lt Fact.out) hk').ne', pow_one]
+    rw [ZMod.val_one'' (one_lt_pow₀ (Nat.Prime.one_lt Fact.out) hk').ne', pow_one]
     exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩

From e109865a902cdb04b1fca0940a97dd30c877dc95 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 5 Mar 2026 22:17:23 -0500
Subject: [PATCH 09/32] fix next file

---
 Mathlib/FieldTheory/Galois/Profinite.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/Galois/Profinite.lean b/Mathlib/FieldTheory/Galois/Profinite.lean
index 9cd3329a9fdbc6..adfed036b81084 100644
--- a/Mathlib/FieldTheory/Galois/Profinite.lean
+++ b/Mathlib/FieldTheory/Galois/Profinite.lean
@@ -168,7 +168,7 @@ theorem restrictNormalHom_continuous (L : IntermediateField k K) [Normal k L] :
     dsimp at this
     rw [hx y.1 ((IntermediateField.mem_lift y).mpr hy)] at this
     exact SetLike.coe_eq_coe.mp this
-  · exact ⟨IntermediateField.fixingSubgroup_isOpen (IntermediateField.lift L'), congrFun rfl⟩
+  · exact ⟨IntermediateField.isOpen_fixingSubgroup (IntermediateField.lift L'), one_mem _⟩
 
 set_option backward.isDefEq.respectTransparency false in
 lemma algEquivToLimit_continuous : Continuous (algEquivToLimit k K) := by

From 6508683dc1f2e82a5370600631c535411676e9f8 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Fri, 6 Mar 2026 15:57:30 -0500
Subject: [PATCH 10/32] prove compactness

---
 Mathlib/FieldTheory/KrullTopology.lean | 63 ++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 645dc1f6a2b635..98ca65ec735389 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -215,6 +215,69 @@ variable (K L) in
 instance krullTopology_discreteTopology_of_finiteDimensional
     [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := inferInstance
 
+variable (K L) in
+set_option backward.isDefEq.respectTransparency false in
+theorem AlgEquiv.totallyBounded_univ : TotallyBounded (Set.univ : Set Gal(L/K)) := by
+  intro U hU
+  rw [krullTopology_mem_uniformity_iff] at hU
+  obtain ⟨F, _, hF⟩ := hU
+  let f (σ : Gal(L/K)) : F →ₐ[K] L := σ.toAlgHom.comp (IsScalarTower.toAlgHom K F L)
+  refine ⟨Set.range (Function.invFun f), Set.finite_range _, fun σ _ => ?_⟩
+  rw [Set.biUnion_range]
+  refine Set.mem_iUnion_of_mem (f σ) (hF σ _ fun x hx => ?_)
+  have hf : f (Function.invFun f (f σ)) ⟨x, hx⟩ = f σ ⟨x, hx⟩ :=
+    DFunLike.congr_fun (Function.invFun_eq ⟨σ, rfl⟩) _
+  simpa [f] using hf.symm
+
+variable (K L) in
+open IntermediateField in
+set_option backward.isDefEq.respectTransparency false in
+instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K) where
+  isCompact_univ := by
+    apply (AlgEquiv.totallyBounded_univ K L).isCompact_of_isComplete
+    intro f hf _
+    rw [cauchy_iff] at hf
+    obtain ⟨_, hf⟩ := hf
+    replace hf (F : IntermediateField K L) (_ : FiniteDimensional K F) :
+        ∃ σ : Gal(L/K), ∀ᶠ τ : Gal(L/K) in f, Set.EqOn σ τ F := by
+      obtain ⟨t, hf, ht⟩ := hf {p | Set.EqOn p.1 p.2 F}
+        (krullTopology_mem_uniformity_iff.2 ⟨F, ‹_›, fun _ _ h => h⟩)
+      obtain ⟨σ, hσ⟩ := Filter.nonempty_of_mem hf
+      exact ⟨σ, Filter.eventually_of_mem hf fun τ hτ => @ht (σ, τ) ⟨hσ, hτ⟩⟩
+    have h (x : L) : ∃ y, ∀ᶠ τ in f, y = τ x :=
+      (hf (adjoin K {x}) (adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x))).elim
+        fun σ hσ => ⟨σ x, hσ.mono fun τ hτ => hτ (mem_adjoin_simple_self K x)⟩
+    choose s hs using h
+    let σ : Gal(L/K) := .ofBijective
+      { toFun := s
+        map_zero' := (hs 0).exists.elim fun _ h => by simp [h]
+        map_one' := (hs 1).exists.elim fun _ h => by simp [h]
+        commutes' x := (hs (algebraMap K L x)).exists.elim fun _ h => by simp [h]
+        map_add' x y := by
+          obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x + y)))).exists
+          simp [hτ.1, hτ.2.1, hτ.2.2]
+        map_mul' x y := by
+          obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x * y)))).exists
+          simp [hτ.1, hτ.2.1, hτ.2.2] } <| by
+      refine ⟨RingHom.injective _, fun x => ?_⟩
+      obtain ⟨τ, hτ⟩ :=
+        ((Filter.eventually_all_finite ((minpoly K x).rootSet_finite L)).2
+          fun y hy => hs y).exists
+      suffices h : τ.symm x ∈ (minpoly K x).rootSet L from ⟨τ.symm x, by simp [hτ (τ.symm x) h]⟩
+      rw [Polynomial.mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)),
+        Polynomial.aeval_algEquiv, AlgHom.comp_apply, minpoly.aeval, map_zero]
+    refine ⟨σ, Set.mem_univ σ, fun U hU => ?_⟩
+    rw [← map_mul_left_nhds_one, Filter.mem_map, krullTopology_mem_nhds_one_iff] at hU
+    obtain ⟨F, _, hF⟩ := hU
+    rw [← Set.image_subset_iff] at hF
+    refine Filter.mem_of_superset ?_ hF
+    obtain ⟨σ', hσ'⟩ := hf F ‹_›
+    have eq : Set.EqOn σ σ' F := fun x hx =>
+      ((hs x).and hσ').exists.elim fun _ h => h.1.trans (h.2 hx).symm
+    filter_upwards [hσ'] with τ hτ using
+      ⟨_, (F.mem_fixingSubgroup_iff _).2 fun x hx =>
+        by simp [AlgEquiv.symm_apply_eq, eq hx, hτ hx], mul_inv_cancel_left σ τ⟩
+
 section MulAction
 
 /-- If `L/K` is an algebraic field extension, then the stabilizer

From 40449b43639643f3b5734a4fccaeb1856f0d6bd8 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 14 May 2026 18:37:11 -0400
Subject: [PATCH 11/32] add comments about deprecation

---
 Mathlib/FieldTheory/KrullTopology.lean | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 45ce19a4c1f23e..6e2e2c706ece40 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -6,8 +6,10 @@ Authors: Sebastian Monnet, Aaron Liu
 module
 
 public import Mathlib.FieldTheory.Galois.Basic
-public import Mathlib.Topology.Algebra.FilterBasis
 public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
+-- this `import` is only used in the deprecated material at the bottom of the file
+-- it should be removed when the deprecated material is removed
+public import Mathlib.Topology.Algebra.FilterBasis
 
 import Mathlib.Topology.Algebra.OpenSubgroup
 import Mathlib.Topology.Connected.Separation
@@ -361,6 +363,13 @@ end IntermediateField
 section deprecated
 set_option linter.deprecated false
 
+/-!
+The definitions and theorems in this section were formerly implementation details
+used in the definition of the Krull topology. Since the Krull topology is now defined in
+terms of the uniform group structure on `Gal(L/K)`, they are now unused,
+and have been deprecated without replacement.
+-/
+
 /-- 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. -/
 @[deprecated "deprecated without replacement" (since := "2026-03-05")]

From 5bd838519a1edcec6617f0bd6a5f3235b2ab0597 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 14 May 2026 18:49:13 -0400
Subject: [PATCH 12/32] update module docstring

---
 Mathlib/FieldTheory/KrullTopology.lean | 26 ++++++++------------------
 1 file changed, 8 insertions(+), 18 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 6e2e2c706ece40..3046957eb4d3e3 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -18,26 +18,13 @@ import Mathlib.Topology.UniformSpace.Separation
 /-!
 # Krull topology
 
-We define the Krull topology on `Gal(L/K)` for an arbitrary field extension `L/K`. In order to do
-this, we first define a `GroupFilterBasis` on `Gal(L/K)`, whose sets are `E.fixingSubgroup` for
-all intermediate fields `E` with `E/K` finite dimensional.
+We define the Krull topology on `Gal(L/K)` for an arbitrary field extension `L/K`, whose basic
+open neighborhoods of `1` are given by `E.fixingSubgroup`, where `E` ranges over intermediate
+field between `L` and `K` such that `E/K` is finite dimensional.
 
 ## Main Definitions
 
-- `finiteExts K L`. Given a field extension `L/K`, this is the set of intermediate fields that are
-  finite-dimensional over `K`.
-
-- `fixedByFinite K L`. Given a field extension `L/K`, `fixedByFinite K L` is the set of
-  subsets `Gal(L/E)` of `Gal(L/K)`, where `E/K` is finite
-
-- `galBasis K L`. Given a field extension `L/K`, this is the filter basis on `Gal(L/K)` whose
-  sets are `Gal(L/E)` for intermediate fields `E` with `E/K` finite.
-
-- `galGroupBasis K L`. This is the same as `galBasis K L`, but with the added structure
-  that it is a group filter basis on `Gal(L/K)`, rather than just a filter basis.
-
-- `krullTopology K L`. Given a field extension `L/K`, this is the topology on `Gal(L/K)`, induced
-  by the group filter basis `galGroupBasis K L`.
+- `krullTopology K L`. Given a field extension `L/K`, this is the topology on `Gal(L/K)`.
 
 ## Main Results
 
@@ -63,7 +50,10 @@ all intermediate fields `E` with `E/K` finite dimensional.
 
 ## Implementation Notes
 
-- `krullTopology K L` is defined as an instance for type class inference.
+We first define a `UniformGroup` structure on `Gal(L/K)`,
+and use this to construct the Krull topology.
+This lets us use the uniform structure to easily prove compactness of the Krull topology,
+by showing it is complete and totally bounded.
 -/
 
 public section

From 6b0f6bc02db07b95038fcb46f11b633eab2cbd71 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Thu, 14 May 2026 18:57:11 -0400
Subject: [PATCH 13/32] fix downstream files

---
 Mathlib/FieldTheory/Galois/Infinite.lean  | 28 ++++-------------------
 Mathlib/FieldTheory/Galois/Profinite.lean |  3 ---
 2 files changed, 5 insertions(+), 26 deletions(-)

diff --git a/Mathlib/FieldTheory/Galois/Infinite.lean b/Mathlib/FieldTheory/Galois/Infinite.lean
index 79a8fa2b713c5e..35e682fd12fc61 100644
--- a/Mathlib/FieldTheory/Galois/Infinite.lean
+++ b/Mathlib/FieldTheory/Galois/Infinite.lean
@@ -21,8 +21,6 @@ closed subgroups of the Galois group.
 
 In `K/k`, for any intermediate field `L` :
 
-* `fixingSubgroup_isClosed` : the subgroup fixing `L` (`Gal(K/L)`) is closed.
-
 * `fixedField_fixingSubgroup` : the field fixed by the
   subgroup fixing `L` is equal to `L` itself.
 
@@ -60,26 +58,10 @@ open scoped Pointwise
 open FiniteGaloisIntermediateField AlgEquiv
 --Note: The `adjoin`s below are `FiniteGaloisIntermediateField.adjoin`
 
+@[deprecated IntermediateField.isClosed_fixingSubgroup (since := "2026-05-14")]
 lemma fixingSubgroup_isClosed (L : IntermediateField k K) [IsGalois k K] :
-    IsClosed (L.fixingSubgroup : Set Gal(K/k)) where
-  isOpen_compl := isOpen_iff_mem_nhds.mpr fun σ h => by
-    apply mem_nhds_iff.mpr
-    rcases Set.not_subset.mp ((mem_fixingSubgroup_iff Gal(K/k)).not.mp h) with ⟨y, yL, ne⟩
-    use σ • ((adjoin k {y}).1.fixingSubgroup : Set Gal(K/k))
-    constructor
-    · intro f hf
-      rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩
-      simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq]
-      apply (mem_fixingSubgroup_iff Gal(K/k)).not.mpr
-      push Not
-      use y
-      simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and]
-      have : g y = y := (mem_fixingSubgroup_iff Gal(K/k)).mp hg y <|
-        adjoin_simple_le_iff.mp le_rfl
-      simpa only [this, ne_eq, AlgEquiv.smul_def] using ne
-    · simp only [(IntermediateField.isOpen_fixingSubgroup (adjoin k {y}).1).smul σ, true_and]
-      use 1
-      simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem]
+    IsClosed (L.fixingSubgroup : Set Gal(K/k)) :=
+  IntermediateField.isClosed_fixingSubgroup L
 
 lemma fixedField_fixingSubgroup (L : IntermediateField k K) [IsGalois k K] :
     IntermediateField.fixedField L.fixingSubgroup = L := by
@@ -190,7 +172,7 @@ lemma fixingSubgroup_fixedField (H : ClosedSubgroup Gal(K/k)) [IsGalois k K] :
 /-- The Galois correspondence from intermediate fields to closed subgroups. -/
 def IntermediateFieldEquivClosedSubgroup [IsGalois k K] :
     IntermediateField k K ≃o (ClosedSubgroup Gal(K/k))ᵒᵈ where
-  toFun L := ⟨L.fixingSubgroup, fixingSubgroup_isClosed L⟩
+  toFun L := ⟨L.fixingSubgroup, L.isClosed_fixingSubgroup⟩
   invFun H := IntermediateField.fixedField H.1
   left_inv L := fixedField_fixingSubgroup L
   right_inv H := by
@@ -203,7 +185,7 @@ def IntermediateFieldEquivClosedSubgroup [IsGalois k K] :
 /-- The Galois correspondence as a `GaloisInsertion` -/
 def GaloisInsertionIntermediateFieldClosedSubgroup [IsGalois k K] :
     GaloisInsertion (OrderDual.toDual ∘ fun (E : IntermediateField k K) ↦
-      (⟨E.fixingSubgroup, fixingSubgroup_isClosed E⟩ : ClosedSubgroup Gal(K/k)))
+      (⟨E.fixingSubgroup, E.isClosed_fixingSubgroup⟩ : ClosedSubgroup Gal(K/k)))
       ((fun (H : ClosedSubgroup Gal(K/k)) ↦ IntermediateField.fixedField H) ∘
         OrderDual.toDual) :=
   OrderIso.toGaloisInsertion IntermediateFieldEquivClosedSubgroup
diff --git a/Mathlib/FieldTheory/Galois/Profinite.lean b/Mathlib/FieldTheory/Galois/Profinite.lean
index 09238a41eadaa6..655d58d1d56802 100644
--- a/Mathlib/FieldTheory/Galois/Profinite.lean
+++ b/Mathlib/FieldTheory/Galois/Profinite.lean
@@ -328,9 +328,6 @@ noncomputable def continuousMulEquivToLimit [IsGalois k K] :
   continuous_toFun := algEquivToLimit_continuous
   continuous_invFun := mulEquivToLimit_symm_continuous
 
-instance [IsGalois k K] : CompactSpace Gal(K/k) :=
-  (continuousMulEquivToLimit k K).symm.compactSpace
-
 /-- `Gal(K/k)` as a profinite group as there is
 a `ContinuousMulEquiv` to a `ProfiniteGrp` given above -/
 noncomputable def profiniteGalGrp [IsGalois k K] : ProfiniteGrp :=

From 21304af99ca9fbe1d0f14ba2850ce9d0a1bbfd67 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sat, 23 May 2026 16:26:09 -0400
Subject: [PATCH 14/32] reminder to remove the import at the top

---
 Mathlib/FieldTheory/KrullTopology.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index cfe9f7216c7a82..30bea5e1b7c731 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -358,6 +358,9 @@ The definitions and theorems in this section were formerly implementation detail
 used in the definition of the Krull topology. Since the Krull topology is now defined in
 terms of the uniform group structure on `Gal(L/K)`, they are now unused,
 and have been deprecated without replacement.
+
+When this section is removed then the `public import Mathlib.Topology.Algebra.FilterBasis` at
+the top of this file should be removed too.
 -/
 
 /-- Given a field extension `L/K`, `finiteExts K L` is the set of

From dde4d1beab274bac5b27b1329040e09ef755904e Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 20 Jul 2026 12:42:02 -0400
Subject: [PATCH 15/32] fix krull topology file

---
 Mathlib/FieldTheory/KrullTopology.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 051056253d3b3c..3922664face236 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -81,7 +81,7 @@ theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} :
   have hf : f.Nonempty := ⟨⊥, inferInstanceAs (FiniteDimensional K (⊥ : IntermediateField K L))⟩
   refine (Filter.mem_biInf_of_directed ?_ hf).trans (by simp [Set.subset_def, Set.EqOn, f])
   intro E hE F hF
-  simp only [Set.mem_setOf_eq, f] at hE hF ⊢
+  simp only [Set.mem_ofPred, f] at hE hF ⊢
   have hl : E ≤ E ⊔ F := le_sup_left
   have hr : F ≤ E ⊔ F := le_sup_right
   exact ⟨E ⊔ F, inferInstance,
@@ -95,7 +95,6 @@ instance krullTopology : TopologicalSpace Gal(L/K) := inferInstance
 
 open IntermediateField in
 variable (K L) in
-set_option backward.isDefEq.respectTransparency false in
 /-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/
 @[stacks 0BMJ "We define the Krull topology directly without proving the universal property"]
 instance : IsUniformGroup Gal(L/K) where
@@ -123,7 +122,7 @@ lemma krullTopology_mem_nhds_one_iff {s : Set Gal(L/K)} : s ∈ 𝓝 1 ↔ ∃ E
   rw [nhds_eq_comap_uniformity', ← le_principal_iff, comap_le_iff_le_kernMap,
     kernMap_principal, le_principal_iff, krullTopology_mem_uniformity_iff]
   refine exists_congr fun F => and_congr_right fun hF => ?_
-  rw [← Prod.forall', ← Set.setOf_subset, Set.subset_kernImage_iff]
+  rw [← Prod.forall', ← Set.ofPred_subset, Set.subset_kernImage_iff]
   exact Iff.of_eq congr($(by ext; simp [Set.EqOn]) ⊆ s)
 
 open scoped Topology in
@@ -203,7 +202,6 @@ instance krullTopology_discreteTopology_of_finiteDimensional
     [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := inferInstance
 
 variable (K L) in
-set_option backward.isDefEq.respectTransparency false in
 theorem AlgEquiv.totallyBounded_univ : TotallyBounded (Set.univ : Set Gal(L/K)) := by
   intro U hU
   rw [krullTopology_mem_uniformity_iff] at hU
@@ -218,7 +216,6 @@ theorem AlgEquiv.totallyBounded_univ : TotallyBounded (Set.univ : Set Gal(L/K))
 
 variable (K L) in
 open IntermediateField in
-set_option backward.isDefEq.respectTransparency false in
 instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K) where
   isCompact_univ := by
     apply (AlgEquiv.totallyBounded_univ K L).isCompact_of_isComplete

From 25cff20224c0655483662e3b8baf6286bfcea058 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 20 Jul 2026 12:57:24 -0400
Subject: [PATCH 16/32] fix cyclotomic character

---
 Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
index 9f63569f5c750d..1efe095719591e 100644
--- a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
+++ b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
@@ -355,8 +355,8 @@ lemma cyclotomicCharacter.continuous (p : ℕ) [Fact p.Prime]
     refine lt_of_le_of_lt ?_ hk
     dsimp
     rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow,
-      RingHom.mem_ker, show ((1 : Gal(L/K)) : L ≃+* L) = 1 from rfl, map_one,
-      map_sub, cyclotomicCharacter.toZModPow, sub_eq_zero, eq_comm, Units.val_one, map_one]
+      RingHom.mem_ker, map_one, map_one, Units.val_one, map_sub, map_one,
+      cyclotomicCharacter.toZModPow, sub_eq_zero, eq_comm]
     apply modularCyclotomicCharacter.unique
     intro t ht
     obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht

From b53c2eb544f4f9f8e7b6f7f79f5c1b8606ed5e11 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sun, 26 Jul 2026 15:11:51 -0400
Subject: [PATCH 17/32] prove

---
 .../Algebra/IsUniformGroup/Basic.lean         | 30 ++++++++++++++++---
 1 file changed, 26 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
index 8f8d8abf600ab1..bcba5fb0f5a684 100644
--- a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
+++ b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
@@ -92,17 +92,39 @@ theorem completeSpace_of_weaklyLocallyCompactSpace
     open scoped RightActions in
     have : f.NeBot := hf.1
     obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
-    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y / x ∈ K := by
-      rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf
+    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y * x⁻¹ ∈ K := by
+      rw [cauchy_iff_le, uniformity_eq_comap_mul_inv_nhds_one, ← tendsto_iff_comap] at hf
       exact hf.eventually_mem K_mem |>.curry.exists
-    simp_rw [div_eq_mul_inv, ← op_smul_eq_mul, MulOpposite.op_inv,
-      ← mem_smul_set_iff_inv_smul_mem] at hx
+    simp_rw [← op_smul_eq_mul, MulOpposite.op_inv, ← mem_smul_set_iff_inv_smul_mem] at hx
     have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete
     obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
     exact ⟨l, hl⟩
 
 end IsRightUniformGroup
 
+namespace IsLeftUniformGroup
+
+variable {G : Type*} [Group G] [UniformSpace G] [IsLeftUniformGroup G]
+
+/-- A locally compact left-uniform group is complete. -/
+@[to_additive
+/-- A locally compact left-uniform additive group is complete. -/]
+theorem completeSpace_of_weaklyLocallyCompactSpace
+    [WeaklyLocallyCompactSpace G] : CompleteSpace G where
+  complete {f} hf := by
+    open scoped RightActions in
+    have : f.NeBot := hf.1
+    obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
+    obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, x⁻¹ * y ∈ K := by
+      rw [cauchy_iff_le, uniformity_eq_comap_inv_mul_nhds_one, ← tendsto_iff_comap] at hf
+      exact hf.eventually_mem K_mem |>.curry.exists
+    simp_rw [← smul_eq_mul, ← mem_smul_set_iff_inv_smul_mem] at hx
+    have Kx_complete : IsComplete (x •> K) := K_compact.smul _ |>.isComplete
+    obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx)
+    exact ⟨l, hl⟩
+
+end IsLeftUniformGroup
+
 namespace Subgroup
 
 @[to_additive]

From f9a23dadcc3a9ce19260c552715fbe6d395a2ea7 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sun, 26 Jul 2026 18:05:48 -0400
Subject: [PATCH 18/32] fix definition

---
 Mathlib/FieldTheory/KrullTopology.lean | 186 ++++++++++++++++---------
 1 file changed, 120 insertions(+), 66 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 3922664face236..e488f481836a2d 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -62,68 +62,115 @@ variable {K L : Type*} [Field K] [Field L] [Algebra K L]
 variable (K L) in
 @[no_expose]
 instance : UniformSpace Gal(L/K) := .ofCore
-  { uniformity := ⨅ (F : IntermediateField K L) (_ : FiniteDimensional K F),
-      𝓟 {p | Set.EqOn p.1 p.2 F}
-    refl := le_iInf₂ fun _ _ =>
-      principal_mono.2 (SetRel.id_subset_iff.2 ⟨fun _ => Set.eqOn_refl _ _⟩)
-    symm := tendsto_iInf_iInf fun _ => tendsto_iInf_iInf fun _ =>
-      Set.MapsTo.tendsto fun _ h => h.symm
-    comp := le_iInf₂ fun F hF =>
-      lift'_le (mem_iInf_of_mem F (mem_iInf_of_mem hF (mem_principal_self _)))
-        (principal_mono.2 (SetRel.isTrans_iff_comp_subset_self.1
-          ⟨fun _ _ _ h₁ h₂ => h₁.trans h₂⟩)) }
+  { uniformity := ⨅ x : L, 𝓟 {p | p.1 x = p.2 x}
+    refl := le_iInf fun _ => principal_mono.2 (SetRel.id_subset_iff.2 ⟨fun _ => rfl⟩)
+    symm := tendsto_iInf_iInf fun _ => Set.MapsTo.tendsto fun _ => Eq.symm
+    comp := le_iInf fun x => lift'_le (mem_iInf_of_mem x (mem_principal_self _))
+      (principal_mono.2 (SetRel.isTrans_iff_comp_subset_self.1 ⟨fun _ _ _ => Eq.trans⟩)) }
+
+theorem krullTopology_uniformity_def : 𝓤 Gal(L/K) = ⨅ x : L, 𝓟 {p | p.1 x = p.2 x} := (rfl)
 
 open SetRel in
 theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} :
-    s ∈ 𝓤 Gal(L/K) ↔ ∃ F : IntermediateField K L,
-      FiniteDimensional K F ∧ ∀ σ τ : Gal(L/K), Set.EqOn σ τ F → σ ~[s] τ := by
-  let f : Set (IntermediateField K L) := {F | FiniteDimensional K F}
-  have hf : f.Nonempty := ⟨⊥, inferInstanceAs (FiniteDimensional K (⊥ : IntermediateField K L))⟩
-  refine (Filter.mem_biInf_of_directed ?_ hf).trans (by simp [Set.subset_def, Set.EqOn, f])
-  intro E hE F hF
-  simp only [Set.mem_ofPred, f] at hE hF ⊢
-  have hl : E ≤ E ⊔ F := le_sup_left
-  have hr : F ≤ E ⊔ F := le_sup_right
-  exact ⟨E ⊔ F, inferInstance,
-    principal_mono.2 fun p h x hx => h (hl hx),
-    principal_mono.2 fun p h x hx => h (hr hx)⟩
+    s ∈ 𝓤 Gal(L/K) ↔ ∃ u : Finset L, ∀ σ τ : Gal(L/K), Set.EqOn σ τ u → σ ~[s] τ := by
+  rw [krullTopology_uniformity_def, Filter.mem_iInf_finite]
+  refine exists_congr fun u => ?_
+  rw [Filter.iInf_principal_finset, Filter.mem_principal, Set.subset_def, Prod.forall]
+  refine forall_congr' fun σ => forall_congr' fun τ => imp_congr_left ?_
+  rw [Set.mem_iInter₂]
+  rfl
 
 variable (K L) in
 /-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
 `Gal(L/K)` induced by the group filter basis `galGroupBasis K L`. -/
 instance krullTopology : TopologicalSpace Gal(L/K) := inferInstance
 
-open IntermediateField in
 variable (K L) in
 /-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/
 @[stacks 0BMJ "We define the Krull topology directly without proving the universal property"]
-instance : IsUniformGroup Gal(L/K) where
-  uniformContinuous_div s hs := by
-    rw [krullTopology_mem_uniformity_iff] at hs
-    obtain ⟨F, _, hF⟩ := hs
-    rw [uniformity_prod_eq_prod, map_map, mem_map, mem_prod_self_iff]
-    refine ⟨{p | Set.EqOn p.1 p.2 (normalClosure K F L)}, ?_, ?_⟩
-    · rw [krullTopology_mem_uniformity_iff]
-      exact ⟨_, inferInstance, fun _ _ h => h⟩
-    rw [Set.prod_subset_iff]
-    intro σ hσ τ hτ
-    simp only [Set.mem_preimage, Function.comp_apply]
-    refine hF _ _ fun x hx => ?_
-    simp only [div_eq_mul_inv, AlgEquiv.mul_apply, AlgEquiv.coe_inv]
-    have hn : τ.1.symm x ∈ normalClosure K F L := by
-      have h : (AlgHom.comp τ.1.symm (IsScalarTower.toAlgHom K F L)).fieldRange ≤
-          normalClosure K F L := AlgHom.fieldRange_le_normalClosure _
-      exact h (by simpa using hx)
-    rw [hσ hn, σ.2.injective.eq_iff, AlgEquiv.eq_symm_apply, ← hτ hn, τ.1.apply_symm_apply]
+instance : IsLeftUniformGroup Gal(L/K) where
+  continuous_mul := by
+    rw [Uniform.continuous_iff'_left]
+    intro p
+    rw [nhds_eq_comap_uniformity', uniformity_prod, comap_inf, comap_comap, comap_comap,
+      krullTopology_uniformity_def, comap_iInf, comap_iInf, tendsto_iInf]
+    intro x
+    rw [tendsto_principal, eventually_inf]
+    refine ⟨{στ | στ.1 (p.2 x) = p.1 (p.2 x)}, ?_, {στ | στ.2 x = p.2 x}, ?_, ?_⟩
+    · exact mem_iInf_of_mem (p.2 x) (by simp)
+    · exact mem_iInf_of_mem x (by simp)
+    · simp +contextual
+  continuous_inv := by
+    rw [Uniform.continuous_iff'_right]
+    intro p
+    rw [nhds_eq_comap_uniformity', krullTopology_uniformity_def, comap_iInf, tendsto_iInf]
+    intro x
+    apply tendsto_iInf' (p.symm x)
+    rw [comap_principal, tendsto_principal_principal]
+    intro σ hp
+    apply σ.eq_symm_apply.mpr
+    simpa using hp
+  uniformity_eq := by
+    rw [nhds_eq_comap_uniformity, comap_comap, krullTopology_uniformity_def, comap_iInf]
+    refine iInf_congr fun x => ?_
+    simp [AlgEquiv.eq_symm_apply]
+
+-- open IntermediateField in
+-- variable (K L) in
+-- /-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/
+-- @[stacks 0BMJ "We define the Krull topology directly without proving the universal property"]
+-- instance : IsUniformGroup Gal(L/K) where
+--   uniformContinuous_div s hs := by
+--     rw [krullTopology_mem_uniformity_iff] at hs
+--     obtain ⟨F, _, hF⟩ := hs
+--     rw [uniformity_prod_eq_prod, map_map, mem_map, mem_prod_self_iff]
+--     refine ⟨{p | Set.EqOn p.1 p.2 (normalClosure K F L)}, ?_, ?_⟩
+--     · rw [krullTopology_mem_uniformity_iff]
+--       exact ⟨_, inferInstance, fun _ _ h => h⟩
+--     rw [Set.prod_subset_iff]
+--     intro σ hσ τ hτ
+--     simp only [Set.mem_preimage, Function.comp_apply]
+--     refine hF _ _ fun x hx => ?_
+--     simp only [div_eq_mul_inv, AlgEquiv.mul_apply, AlgEquiv.coe_inv]
+--     have hn : τ.1.symm x ∈ normalClosure K F L := by
+--       have h : (AlgHom.comp τ.1.symm (IsScalarTower.toAlgHom K F L)).fieldRange ≤
+--           normalClosure K F L := AlgHom.fieldRange_le_normalClosure _
+--       exact h (by simpa using hx)
+--     rw [hσ hn, σ.2.injective.eq_iff, AlgEquiv.eq_symm_apply, ← hτ hn, τ.1.apply_symm_apply]
 
+open IntermediateField in
 open scoped Topology in
-lemma krullTopology_mem_nhds_one_iff {s : Set Gal(L/K)} : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
-    FiniteDimensional K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by
+lemma krullTopology_mem_nhds_one_iff' {s : Set Gal(L/K)} :
+    s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, E.FG ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by
   rw [nhds_eq_comap_uniformity', ← le_principal_iff, comap_le_iff_le_kernMap,
     kernMap_principal, le_principal_iff, krullTopology_mem_uniformity_iff]
-  refine exists_congr fun F => and_congr_right fun hF => ?_
-  rw [← Prod.forall', ← Set.ofPred_subset, Set.subset_kernImage_iff]
-  exact Iff.of_eq congr($(by ext; simp [Set.EqOn]) ⊆ s)
+  simp_rw [← Prod.forall', ← Set.ofPred_subset_ofPred, Prod.eta, Set.ofPred_mem_eq,
+    Set.subset_kernImage_iff, Set.preimage_ofPred_eq, Set.ofPred_subset,
+    FG, existsAndEq, true_and, Set.subset_def, SetLike.mem_coe,
+    IntermediateField.mem_fixingSubgroup_iff, Set.EqOn, AlgEquiv.one_apply]
+  refine exists_congr fun u => forall_congr' fun σ => imp_congr_left ?_
+  revert σ
+  have hst (σ : Gal(L/K)) (x : L) : σ x = x ↔ x ∈ fixedField (Subgroup.zpowers σ) := by
+    rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← adjoin_le_iff, le_iff_le,
+      Subgroup.zpowers_le, ← AlgEquiv.smul_def, ← MulAction.mem_stabilizer_iff]
+    revert σ
+    rw [← SetLike.ext_iff, le_antisymm_iff, ← le_iff_le, adjoin_simple_le_iff]
+    constructor
+    · simp
+    · intro σ hσ
+      simpa using hσ ⟨x, mem_adjoin_simple_self K x⟩
+  simp_rw [hst, ← Set.ofPred_subset_ofPred, SetLike.setOfPred_mem_eq,
+    Set.ofPred_mem_eq, SetLike.coe_subset_coe, adjoin_le_iff, forall_true_iff]
+
+open IntermediateField in
+open scoped Topology in
+lemma krullTopology_mem_nhds_one_iff [Algebra.IsAlgebraic K L] {s : Set Gal(L/K)} :
+    s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L,
+    FiniteDimensional K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by
+  rw [krullTopology_mem_nhds_one_iff']
+  refine exists_congr fun E => and_congr_left' ?_
+  rw [← IntermediateField.essFiniteType_iff]
+  exact ⟨fun _ => Algebra.finite_of_essFiniteType_of_isAlgebraic, fun _ => inferInstance⟩
 
 open scoped Topology in
 lemma krullTopology_mem_nhds_one_iff_of_normal [Normal K L] {s : Set Gal(L/K)} :
@@ -142,19 +189,20 @@ open scoped Topology Filter
 /-- Let `L/E/K` be a tower of fields with `E/K` finite.
 Then `Gal(L/E)` is an open subgroup of `Gal(L/K)`. -/
 theorem IntermediateField.isOpen_fixingSubgroup (E : IntermediateField K L)
-    [FiniteDimensional K E] : IsOpen (E.fixingSubgroup : Set Gal(L/K)) :=
-  Subgroup.isOpen_of_mem_nhds _ (krullTopology_mem_nhds_one_iff.2 ⟨E, ‹_›, subset_rfl⟩)
+    [Algebra.EssFiniteType K E] : IsOpen (E.fixingSubgroup : Set Gal(L/K)) :=
+  Subgroup.isOpen_of_mem_nhds _ (krullTopology_mem_nhds_one_iff'.2
+    ⟨E, essFiniteType_iff.1 ‹_›, subset_rfl⟩)
 
 @[deprecated (since := "2026-03-05")]
 alias IntermediateField.fixingSubgroup_isOpen := IntermediateField.isOpen_fixingSubgroup
 
 /-- Given a tower of fields `L/E/K`, with `E/K` finite,
 the subgroup `Gal(L/E) ≤ Gal(L/K)` is closed. -/
-theorem IntermediateField.isClosed_fixingSubgroup (E : IntermediateField K L)
-    [Algebra.IsIntegral K E] : IsClosed (E.fixingSubgroup : Set Gal(L/K)) := by
+theorem IntermediateField.isClosed_fixingSubgroup (E : IntermediateField K L) :
+    IsClosed (E.fixingSubgroup : Set Gal(L/K)) := by
   have hx (x : E) : IsClosed ((adjoin K {(x : L)}).fixingSubgroup : Set Gal(L/K)) :=
-    have : FiniteDimensional K (adjoin K {(x : L)}) := IntermediateField.adjoin.finiteDimensional
-      (coe_isIntegral_iff.2 (Algebra.IsIntegral.isIntegral x))
+    have : Algebra.EssFiniteType K (adjoin K {(x : L)}) :=
+      essFiniteType_iff.2 (fg_adjoin_of_finite (Set.finite_singleton _))
     Subgroup.isClosed_of_isOpen _ (isOpen_fixingSubgroup _)
   convert isClosed_iInter hx
   ext g
@@ -169,14 +217,15 @@ end KrullT2
 
 section TotallySeparated
 
-instance [Algebra.IsIntegral K L] : TotallySeparatedSpace Gal(L/K) := by
+instance : TotallySeparatedSpace Gal(L/K) := by
   rw [totallySeparatedSpace_iff_exists_isClopen]
   intro σ τ h_diff
   have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one]
   rcases DFunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩
   let E := IntermediateField.adjoin K ({x} : Set L)
-  have := IntermediateField.adjoin.finiteDimensional
-    (Algebra.IsIntegral.isIntegral (R := K) x)
+  have fg : Algebra.EssFiniteType K E :=
+    IntermediateField.essFiniteType_iff.2
+      (IntermediateField.fg_adjoin_of_finite (Set.finite_singleton _))
   refine ⟨σ • E.fixingSubgroup,
     ⟨E.isClosed_fixingSubgroup.leftCoset σ, E.isOpen_fixingSubgroup.leftCoset σ⟩,
     ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩
@@ -185,32 +234,36 @@ instance [Algebra.IsIntegral K L] : TotallySeparatedSpace Gal(L/K) := by
   exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
 
 /-- If `L/K` is an algebraic extension, then the Krull topology on `Gal(L/K)` is Hausdorff. -/
-instance krullTopology_t2 [Algebra.IsIntegral K L] : T2Space Gal(L/K) :=
-  TotallySeparatedSpace.t2Space
+instance krullTopology_t2 : T2Space Gal(L/K) := TotallySeparatedSpace.t2Space
 
 /-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is
   totally separated. -/
 @[deprecated TotallySeparatedSpace.isTotallySeparated_univ (since := "2026-03-05")]
-theorem krullTopology_isTotallySeparated [Algebra.IsIntegral K L] :
+theorem krullTopology_isTotallySeparated :
     IsTotallySeparated (Set.univ : Set Gal(L/K)) :=
   (totallySeparatedSpace_iff _).mp inferInstance
 
 end TotallySeparated
 
 variable (K L) in
-instance krullTopology_discreteTopology_of_finiteDimensional
-    [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := inferInstance
+instance krullTopology_discreteTopology_of_essFiniteType
+    [Algebra.EssFiniteType K L] : DiscreteTopology Gal(L/K) := sorry
 
 variable (K L) in
-theorem AlgEquiv.totallyBounded_univ : TotallyBounded (Set.univ : Set Gal(L/K)) := by
+theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :
+    TotallyBounded (Set.univ : Set Gal(L/K)) := by
   intro U hU
   rw [krullTopology_mem_uniformity_iff] at hU
-  obtain ⟨F, _, hF⟩ := hU
+  obtain ⟨s, hs⟩ := hU
+  let F := IntermediateField.adjoin K (s : Set L)
+  have : FiniteDimensional K F :=
+    IntermediateField.finiteDimensional_adjoin fun _ _ => Algebra.IsIntegral.isIntegral _
   let f (σ : Gal(L/K)) : F →ₐ[K] L := σ.toAlgHom.comp (IsScalarTower.toAlgHom K F L)
   refine ⟨Set.range (Function.invFun f), Set.finite_range _, fun σ _ => ?_⟩
   rw [Set.biUnion_range]
-  refine Set.mem_iUnion_of_mem (f σ) (hF σ _ fun x hx => ?_)
-  have hf : f (Function.invFun f (f σ)) ⟨x, hx⟩ = f σ ⟨x, hx⟩ :=
+  refine Set.mem_iUnion_of_mem (f σ) (hs σ _ fun x hx => ?_)
+  have hf : f (Function.invFun f (f σ)) ⟨x, IntermediateField.mem_adjoin_of_mem K hx⟩ =
+      f σ ⟨x, IntermediateField.mem_adjoin_of_mem K hx⟩ :=
     DFunLike.congr_fun (Function.invFun_eq ⟨σ, rfl⟩) _
   simpa [f] using hf.symm
 
@@ -266,11 +319,12 @@ section MulAction
 
 /-- If `L/K` is an algebraic field extension, then the stabilizer
 in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/
-theorem stabilizer_isOpen_of_isIntegral [Algebra.IsIntegral K L] (x : L) :
+theorem stabilizer_isOpen_of_isIntegral (x : L) :
     IsOpen (MulAction.stabilizer Gal(L/K) x : Set Gal(L/K)) := by
   open IntermediateField in
   let E := adjoin K {x}
-  have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x)
+  have hL : Algebra.EssFiniteType K E := IntermediateField.essFiniteType_iff.2
+    (IntermediateField.fg_adjoin_of_finite (Set.finite_singleton _))
   convert! isOpen_fixingSubgroup E
   ext g
   simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm

From f5c90435e45a14505622fd3226eac61c1878ac91 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sun, 26 Jul 2026 18:05:55 -0400
Subject: [PATCH 19/32] fix docstrings

---
 Mathlib/FieldTheory/KrullTopology.lean | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index e488f481836a2d..aaea147205d10c 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -20,7 +20,7 @@ import Mathlib.Topology.UniformSpace.Separation
 
 We define the Krull topology on `Gal(L/K)` for an arbitrary field extension `L/K`, whose basic
 open neighborhoods of `1` are given by `E.fixingSubgroup`, where `E` ranges over intermediate
-field between `L` and `K` such that `E/K` is finite dimensional.
+field between `L` and `K` such that `E/K` is finitely generated.
 
 ## Main Definitions
 
@@ -60,6 +60,7 @@ open scoped Pointwise Uniformity
 variable {K L : Type*} [Field K] [Field L] [Algebra K L]
 
 variable (K L) in
+/-- For a field extension `L/K`, we equiv `Gal(L/K)` with the left uniform structure. -/
 @[no_expose]
 instance : UniformSpace Gal(L/K) := .ofCore
   { uniformity := ⨅ x : L, 𝓟 {p | p.1 x = p.2 x}
@@ -82,7 +83,7 @@ theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} :
 
 variable (K L) in
 /-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
-`Gal(L/K)` induced by the group filter basis `galGroupBasis K L`. -/
+`Gal(L/K)` induced by the uniform structure. -/
 instance krullTopology : TopologicalSpace Gal(L/K) := inferInstance
 
 variable (K L) in
@@ -186,7 +187,7 @@ section KrullT2
 
 open scoped Topology Filter
 
-/-- Let `L/E/K` be a tower of fields with `E/K` finite.
+/-- Let `L/E/K` be a tower of fields with `E/K` finitely generated.
 Then `Gal(L/E)` is an open subgroup of `Gal(L/K)`. -/
 theorem IntermediateField.isOpen_fixingSubgroup (E : IntermediateField K L)
     [Algebra.EssFiniteType K E] : IsOpen (E.fixingSubgroup : Set Gal(L/K)) :=
@@ -196,8 +197,7 @@ theorem IntermediateField.isOpen_fixingSubgroup (E : IntermediateField K L)
 @[deprecated (since := "2026-03-05")]
 alias IntermediateField.fixingSubgroup_isOpen := IntermediateField.isOpen_fixingSubgroup
 
-/-- Given a tower of fields `L/E/K`, with `E/K` finite,
-the subgroup `Gal(L/E) ≤ Gal(L/K)` is closed. -/
+/-- Given a tower of fields `L/E/K`, the subgroup `Gal(L/E) ≤ Gal(L/K)` is closed. -/
 theorem IntermediateField.isClosed_fixingSubgroup (E : IntermediateField K L) :
     IsClosed (E.fixingSubgroup : Set Gal(L/K)) := by
   have hx (x : E) : IsClosed ((adjoin K {(x : L)}).fixingSubgroup : Set Gal(L/K)) :=
@@ -233,11 +233,10 @@ instance : TotallySeparatedSpace Gal(L/K) := by
     IntermediateField.mem_fixingSubgroup_iff, not_forall]
   exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩
 
-/-- If `L/K` is an algebraic extension, then the Krull topology on `Gal(L/K)` is Hausdorff. -/
+/-- The Krull topology on `Gal(L/K)` is Hausdorff. -/
 instance krullTopology_t2 : T2Space Gal(L/K) := TotallySeparatedSpace.t2Space
 
-/-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is
-  totally separated. -/
+/-- The Krull topology on `Gal(L/K)` is totally separated. -/
 @[deprecated TotallySeparatedSpace.isTotallySeparated_univ (since := "2026-03-05")]
 theorem krullTopology_isTotallySeparated :
     IsTotallySeparated (Set.univ : Set Gal(L/K)) :=
@@ -246,8 +245,8 @@ theorem krullTopology_isTotallySeparated :
 end TotallySeparated
 
 variable (K L) in
-instance krullTopology_discreteTopology_of_essFiniteType
-    [Algebra.EssFiniteType K L] : DiscreteTopology Gal(L/K) := sorry
+instance krullTopology_discreteUniformity_of_essFiniteType
+    [Algebra.EssFiniteType K L] : DiscreteUniformity Gal(L/K) := sorry
 
 variable (K L) in
 theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :
@@ -271,6 +270,7 @@ variable (K L) in
 open IntermediateField in
 instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K) where
   isCompact_univ := by
+    stop
     apply (AlgEquiv.totallyBounded_univ K L).isCompact_of_isComplete
     intro f hf _
     rw [cauchy_iff] at hf
@@ -317,8 +317,7 @@ instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K) where
 
 section MulAction
 
-/-- If `L/K` is an algebraic field extension, then the stabilizer
-in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/
+/-- The stabilizer in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/
 theorem stabilizer_isOpen_of_isIntegral (x : L) :
     IsOpen (MulAction.stabilizer Gal(L/K) x : Set Gal(L/K)) := by
   open IntermediateField in

From acfc52e4848acb74da42bfaacac5739fbf0edb59 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sun, 26 Jul 2026 18:33:04 -0400
Subject: [PATCH 20/32] prove more theorem

---
 Mathlib/FieldTheory/KrullTopology.lean | 32 +++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index aaea147205d10c..a8e829b24d267d 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -246,7 +246,37 @@ end TotallySeparated
 
 variable (K L) in
 instance krullTopology_discreteUniformity_of_essFiniteType
-    [Algebra.EssFiniteType K L] : DiscreteUniformity Gal(L/K) := sorry
+    [Algebra.EssFiniteType K L] : DiscreteUniformity Gal(L/K) := by
+  rw [discreteUniformity_iff_eq_principal_setRelId, le_antisymm_iff,
+    and_iff_left refl_le_uniformity, krullTopology_uniformity_def]
+  obtain ⟨s, hs⟩ := IntermediateField.fg_top K L
+  rw [Filter.le_principal_iff, Filter.mem_iInf_finite]
+  refine ⟨s, ?_⟩
+  rw [Filter.iInf_principal_finset, Filter.mem_principal]
+  intro p hp
+  rw [Set.mem_iInter₂] at hp
+  have hpe (x : L) : p.1 x = p.2 x ↔
+      x ∈ IntermediateField.fixedField (Subgroup.zpowers (p.1⁻¹ * p.2)) := by
+    rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← IntermediateField.adjoin_le_iff,
+      IntermediateField.le_iff_le, Subgroup.zpowers_le, ← p.1.eq_symm_apply,
+      ← AlgEquiv.coe_inv, ← AlgEquiv.mul_apply, ← AlgEquiv.smul_def, eq_comm,
+      ← MulAction.mem_stabilizer_iff]
+    generalize p.1⁻¹ * p.2 = σ
+    revert σ
+    rw [← SetLike.ext_iff, le_antisymm_iff, ← IntermediateField.le_iff_le,
+      IntermediateField.adjoin_simple_le_iff]
+    constructor
+    · simp
+    · intro σ hσ
+      simpa using hσ ⟨x, IntermediateField.mem_adjoin_simple_self K x⟩
+  ext x
+  have hx : x ∈ (⊤ : IntermediateField K L) := IntermediateField.mem_top
+  rw [hpe]
+  revert x hx
+  rw [← SetLike.le_def, ← hs, IntermediateField.adjoin_le_iff]
+  intro x hx
+  rw [SetLike.mem_coe, ← hpe]
+  exact hp x hx
 
 variable (K L) in
 theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :

From 596fe4e7e786ec60c87e2e11a6679b12c2198cdd Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sun, 26 Jul 2026 19:09:19 -0400
Subject: [PATCH 21/32] test: low priority instance

---
 Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
index bcba5fb0f5a684..da75294d0e6fb9 100644
--- a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
+++ b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
@@ -86,7 +86,7 @@ variable {G : Type*} [Group G] [UniformSpace G] [IsRightUniformGroup G]
 /-- A locally compact right-uniform group is complete. -/
 @[to_additive
 /-- A locally compact right-uniform additive group is complete. -/]
-theorem completeSpace_of_weaklyLocallyCompactSpace
+instance (priority := 100) completeSpace_of_weaklyLocallyCompactSpace
     [WeaklyLocallyCompactSpace G] : CompleteSpace G where
   complete {f} hf := by
     open scoped RightActions in
@@ -109,7 +109,7 @@ variable {G : Type*} [Group G] [UniformSpace G] [IsLeftUniformGroup G]
 /-- A locally compact left-uniform group is complete. -/
 @[to_additive
 /-- A locally compact left-uniform additive group is complete. -/]
-theorem completeSpace_of_weaklyLocallyCompactSpace
+instance (priority := 100) completeSpace_of_weaklyLocallyCompactSpace
     [WeaklyLocallyCompactSpace G] : CompleteSpace G where
   complete {f} hf := by
     open scoped RightActions in

From ad3c4075866491f9cd15778c386844c4e57ca6ea Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Sun, 26 Jul 2026 19:38:32 -0400
Subject: [PATCH 22/32] uninstance

---
 Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
index da75294d0e6fb9..e01cc473283d70 100644
--- a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
+++ b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean
@@ -86,7 +86,8 @@ variable {G : Type*} [Group G] [UniformSpace G] [IsRightUniformGroup G]
 /-- A locally compact right-uniform group is complete. -/
 @[to_additive
 /-- A locally compact right-uniform additive group is complete. -/]
-instance (priority := 100) completeSpace_of_weaklyLocallyCompactSpace
+-- not an instance for performance reasons, see benchmark on PR #42117
+theorem completeSpace_of_weaklyLocallyCompactSpace
     [WeaklyLocallyCompactSpace G] : CompleteSpace G where
   complete {f} hf := by
     open scoped RightActions in
@@ -109,7 +110,8 @@ variable {G : Type*} [Group G] [UniformSpace G] [IsLeftUniformGroup G]
 /-- A locally compact left-uniform group is complete. -/
 @[to_additive
 /-- A locally compact left-uniform additive group is complete. -/]
-instance (priority := 100) completeSpace_of_weaklyLocallyCompactSpace
+-- not an instance for performance reasons, see benchmark on PR #42117
+theorem completeSpace_of_weaklyLocallyCompactSpace
     [WeaklyLocallyCompactSpace G] : CompleteSpace G where
   complete {f} hf := by
     open scoped RightActions in

From a574a21a0e2a03c7ac3016c50628da460aa3b983 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 08:41:37 -0400
Subject: [PATCH 23/32] generalize totally bounded

---
 Mathlib/FieldTheory/KrullTopology.lean | 34 +++++++++++++++++---------
 1 file changed, 22 insertions(+), 12 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index a8e829b24d267d..3ed9d6026c3be4 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -278,23 +278,33 @@ instance krullTopology_discreteUniformity_of_essFiniteType
   rw [SetLike.mem_coe, ← hpe]
   exact hp x hx
 
-variable (K L) in
-theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :
-    TotallyBounded (Set.univ : Set Gal(L/K)) := by
+theorem AlgEquiv.totallyBounded_fixingSubgroup
+    (E : IntermediateField K L) [Algebra.IsAlgebraic E L] :
+    TotallyBounded (E.fixingSubgroup : Set Gal(L/K)) := by
   intro U hU
   rw [krullTopology_mem_uniformity_iff] at hU
   obtain ⟨s, hs⟩ := hU
-  let F := IntermediateField.adjoin K (s : Set L)
-  have : FiniteDimensional K F :=
+  let F := IntermediateField.adjoin E (s : Set L)
+  have : IsScalarTower K F L := ⟨fun a b c => smul_assoc a b.1 c⟩
+  have : FiniteDimensional E F :=
     IntermediateField.finiteDimensional_adjoin fun _ _ => Algebra.IsIntegral.isIntegral _
-  let f (σ : Gal(L/K)) : F →ₐ[K] L := σ.toAlgHom.comp (IsScalarTower.toAlgHom K F L)
-  refine ⟨Set.range (Function.invFun f), Set.finite_range _, fun σ _ => ?_⟩
+  let f (σ : Gal(L/E)) : F →ₐ[E] L := σ.toAlgHom.comp (IsScalarTower.toAlgHom E F L)
+  refine ⟨Set.range (AlgEquiv.restrictScalars K ∘ Function.invFun f),
+    Set.finite_range _, fun σ hσ => ?_⟩
+  let σE := E.fixingSubgroupEquiv ⟨σ, hσ⟩
   rw [Set.biUnion_range]
-  refine Set.mem_iUnion_of_mem (f σ) (hs σ _ fun x hx => ?_)
-  have hf : f (Function.invFun f (f σ)) ⟨x, IntermediateField.mem_adjoin_of_mem K hx⟩ =
-      f σ ⟨x, IntermediateField.mem_adjoin_of_mem K hx⟩ :=
-    DFunLike.congr_fun (Function.invFun_eq ⟨σ, rfl⟩) _
-  simpa [f] using hf.symm
+  refine Set.mem_iUnion_of_mem (f σE) (hs σ _ fun x hx => ?_)
+  let xE : F := ⟨x, IntermediateField.mem_adjoin_of_mem E hx⟩
+  have hf : f (Function.invFun f (f σE)) xE = f σE xE :=
+    DFunLike.congr_fun (Function.invFun_eq ⟨σE, rfl⟩) xE
+  -- TODO: add API for `IntermediateField.fixingSubgroup`
+  simpa [f, σE, xE, IntermediateField.fixingSubgroupEquiv] using hf.symm
+
+variable (K L) in
+theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :
+    TotallyBounded (Set.univ : Set Gal(L/K)) := by
+  rw [← Subgroup.coe_top, ← IntermediateField.fixingSubgroup_bot]
+  exact AlgEquiv.totallyBounded_fixingSubgroup ⊥
 
 variable (K L) in
 open IntermediateField in

From fd3a72a3655a6a98f237fa4f6f80b216568d169f Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 09:47:42 -0400
Subject: [PATCH 24/32] add theorems

---
 Mathlib/FieldTheory/Galois/Basic.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean
index ca7c4c787c1f51..89aa72f61ae6ec 100644
--- a/Mathlib/FieldTheory/Galois/Basic.lean
+++ b/Mathlib/FieldTheory/Galois/Basic.lean
@@ -270,6 +270,16 @@ def fixingSubgroupEquiv : fixingSubgroup K ≃* Gal(E/K) where
   invFun ϕ := ⟨ϕ.restrictScalars _, ϕ.commutes⟩
   map_mul' _ _ := by ext; rfl
 
+@[simp]
+theorem coe_fixingSubgroupEquiv_apply (σ : K.fixingSubgroup) :
+    ⇑(K.fixingSubgroupEquiv σ) = ⇑σ.1 :=
+  rfl
+
+@[simp]
+theorem coe_fixingSubgroupEquiv_symm_apply (σ : Gal(E/K)) :
+    ⇑(K.fixingSubgroupEquiv.symm σ).1 = ⇑σ :=
+  rfl
+
 theorem fixingSubgroup_fixedField [FiniteDimensional F E] : fixingSubgroup (fixedField H) = H := by
   have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl
   suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by
@@ -288,6 +298,16 @@ def subgroupEquivAlgEquiv [FiniteDimensional F E] (H : Subgroup Gal(E/F)) :
     H ≃* Gal(E/IntermediateField.fixedField H) :=
   (MulEquiv.subgroupCongr (fixingSubgroup_fixedField H).symm).trans (fixingSubgroupEquiv _)
 
+@[simp]
+theorem coe_subgroupEquivAlgEquiv_apply [FiniteDimensional F E] (σ : H) :
+    ⇑(subgroupEquivAlgEquiv H σ) = ⇑σ.1 :=
+  rfl
+
+@[simp]
+theorem coe_subgroupEquivAlgEquiv_symm_apply [FiniteDimensional F E] (σ : Gal(E/fixedField H)) :
+    ⇑((subgroupEquivAlgEquiv H).symm σ).1 = ⇑σ :=
+  rfl
+
 instance fixedField.smul : SMul K (fixedField (fixingSubgroup K)) where
   smul x y := ⟨x * y, fun ϕ => by
     rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]⟩

From 05aabb446a367c68edf6f658db97fe247a3bf254 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 12:07:39 -0400
Subject: [PATCH 25/32] new file

---
 Mathlib.lean                                  |  1 +
 Mathlib/FieldTheory/FinTrdeg.lean             | 91 +++++++++++++++++++
 .../IntermediateField/Adjoin/Basic.lean       | 12 +++
 .../TranscendenceBasis.lean                   |  2 +-
 4 files changed, 105 insertions(+), 1 deletion(-)
 create mode 100644 Mathlib/FieldTheory/FinTrdeg.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 624f35d65fc813..2d93584d606e31 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -4517,6 +4517,7 @@ public import Mathlib.FieldTheory.ChevalleyWarning
 public import Mathlib.FieldTheory.Differential.Basic
 public import Mathlib.FieldTheory.Differential.Liouville
 public import Mathlib.FieldTheory.Extension
+public import Mathlib.FieldTheory.FinTrdeg
 public import Mathlib.FieldTheory.Finite.Basic
 public import Mathlib.FieldTheory.Finite.Extension
 public import Mathlib.FieldTheory.Finite.GaloisField
diff --git a/Mathlib/FieldTheory/FinTrdeg.lean b/Mathlib/FieldTheory/FinTrdeg.lean
new file mode 100644
index 00000000000000..310b323fdb7f34
--- /dev/null
+++ b/Mathlib/FieldTheory/FinTrdeg.lean
@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2026 Aaron Liu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Aaron Liu
+-/
+module
+
+public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
+public import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
+public import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
+
+/-!
+# Extensions with Finite Transcendence Degree
+
+A field extension L/K has finite transcendence degree if
+the transcendence degree of L over K is finite.
+Equivalently, if L is an algebraic extension of a finitely generated field extension of K.
+-/
+
+public section
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
+
+open IntermediateField
+
+variable (K L) in
+/-- A field extension L/K is said to have finite transcendence degree if there is some
+intermediate extension L/E/K with E/K finitely generated and L/E algebraic. -/
+class FinTrdeg where
+  exists_fg_isAlgebraic : ∃ E : IntermediateField K L, E.FG ∧ Algebra.IsAlgebraic E L
+
+variable (K L) in
+instance [Algebra.IsAlgebraic K L] : FinTrdeg K L where
+  exists_fg_isAlgebraic := ⟨⊥, IntermediateField.fg_bot, inferInstance⟩
+
+variable (K L) in
+instance [Algebra.EssFiniteType K L] : FinTrdeg K L where
+  exists_fg_isAlgebraic := ⟨⊤, IntermediateField.fg_top_iff.mpr ‹_›, inferInstance⟩
+
+theorem finTrdeg_iff_trdeg : FinTrdeg K L ↔ Algebra.trdeg K L < .aleph0 := by
+  constructor
+  · intro ⟨E, fg, alg⟩
+    rw [← trdeg_add_eq K E, trdeg_eq_zero_iff.2 alg, add_zero]
+    rw [← essFiniteType_iff, Algebra.essFiniteType_iff_exists_subalgebra] at fg
+    obtain ⟨S₀, M, fin, islocal⟩ := fg
+    rw [← trdeg_add_eq K S₀, trdeg_eq_zero_iff.2 islocal.isAlgebraic, add_zero]
+    exact trdeg_lt_aleph0_of_finiteType
+  · intro h
+    obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L
+    have fin : s.Finite := Cardinal.lt_aleph0_iff_set_finite.1 (hs.cardinalMk_eq_trdeg.trans_lt h)
+    constructor
+    refine ⟨adjoin K s, fg_adjoin_of_finite fin, ?_⟩
+    have alg := hs.isAlgebraic_field
+    rwa [Subtype.range_coe] at alg
+
+alias ⟨_, FinTrdeg.of_trdeg⟩ := finTrdeg_iff_trdeg
+
+variable (K L) in
+theorem trdeg_lt_aleph0 [FinTrdeg K L] : Algebra.trdeg K L < .aleph0 :=
+  finTrdeg_iff_trdeg.mp ‹_›
+
+theorem FinTrdeg.trans (K E L : Type*) [Field K] [Field E] [Field L]
+    [Algebra K E] [Algebra K L] [Algebra E L] [IsScalarTower K E L]
+    [FinTrdeg K E] [FinTrdeg E L] : FinTrdeg K L := by
+  rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0, ← lift_trdeg_add_eq K E L,
+    Cardinal.add_lt_aleph0_iff, Cardinal.lift_lt_aleph0, Cardinal.lift_lt_aleph0]
+  exact ⟨trdeg_lt_aleph0 K E, trdeg_lt_aleph0 E L⟩
+
+theorem finite_of_isTranscendenceBasis [FinTrdeg K L] {ι : Type*} {x : ι → L}
+    (hx : IsTranscendenceBasis K x) : Finite ι := by
+  rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0,
+    hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]
+  exact trdeg_lt_aleph0 K L
+
+theorem finite_of_algebraicIndependent [FinTrdeg K L] {ι : Type*} {x : ι → L}
+    (hx : AlgebraicIndependent K x) : Finite ι := by
+  rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0]
+  exact hx.lift_cardinalMk_le_trdeg.trans_lt (Cardinal.lift_lt_aleph0.mpr (trdeg_lt_aleph0 K L))
+
+theorem FinTrdeg.of_isTranscendenceBasis {ι : Type*} [Finite ι] {x : ι → L}
+    (hx : IsTranscendenceBasis K x) : FinTrdeg K L := by
+  rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0,
+    ← hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]
+  exact Cardinal.mk_lt_aleph0
+
+theorem exists_finset_isTranscendenceBasis [FinTrdeg K L] :
+    ∃ s : Finset L, IsTranscendenceBasis K ((↑) : s → L) := by
+  obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L
+  obtain ⟨s, rfl⟩ := Finset.mem_range_coe_iff.2
+    (Set.finite_coe_iff.1 (finite_of_isTranscendenceBasis hs))
+  exact ⟨s, hs⟩
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
index e29255c21b390a..e02ae0d68e269b 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
@@ -554,6 +554,18 @@ theorem _root_.Polynomial.Irreducible.natDegree_dvd_finrank {f : K[X]} (hi : Irr
   contrapose hi
   rwa [hi, mul_zero] at key
 
+instance : Algebra.IsAlgebraic K (⊥ : IntermediateField K L) where
+  isAlgebraic := by
+    intro ⟨x, hx⟩
+    obtain ⟨c, rfl⟩ := hx
+    exact isAlgebraic_algebraMap c
+
+instance : Algebra.IsAlgebraic (⊤ : IntermediateField K L) L where
+  isAlgebraic := by
+    intro x
+    let xt : (⊤ : IntermediateField K L) := ⟨x, mem_top⟩
+    exact isAlgebraic_algebraMap xt
+
 -- TODO: generalize to `Sort`
 /-- A compositum of algebraic extensions is algebraic -/
 theorem isAlgebraic_iSup {ι : Type*} {t : ι → IntermediateField K L}
diff --git a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
index 3fc6d888aef1fc..4fbff1f01e5b53 100644
--- a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
+++ b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
@@ -451,7 +451,7 @@ theorem Polynomial.trdeg_of_isDomain [IsDomain R] : trdeg R (Polynomial R) = 1 :
   simpa using (IsTranscendenceBasis.polynomial Unit R).lift_cardinalMk_eq_trdeg.symm
 
 -- TODO: generalize to Nontrivial S
-theorem trdeg_lt_aleph0 [IsDomain R] [fin : FiniteType R S] : trdeg R S < ℵ₀ :=
+theorem trdeg_lt_aleph0_of_finiteType [IsDomain R] [fin : FiniteType R S] : trdeg R S < ℵ₀ :=
   have ⟨n, f, surj⟩ := FiniteType.iff_quotient_mvPolynomial''.mp fin
   lift_lt.mp <| (lift_trdeg_le_of_surjective f surj).trans_lt <| by simp
 

From 33495b6ead787b99cd72859e40735fe368d5d86e Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 13:17:38 -0400
Subject: [PATCH 26/32] more instances

---
 Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean | 3 +++
 Mathlib/RingTheory/FiniteType.lean                        | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
index 4356fb001bd12b..467724c83aa967 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
@@ -124,6 +124,9 @@ lemma essFiniteType_iff {K : IntermediateField F E} :
       adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using! this
   exact ⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩
 
+instance [Finite S] : Algebra.EssFiniteType F (adjoin F S) :=
+  essFiniteType_iff.mpr (fg_adjoin_of_finite S.toFinite)
+
 /-- A field is finitely generated if and only if it is essentially of finite type over its prime
 subfield. -/
 theorem _root_.Field.fg_iff_essFiniteType : Field.FG F ↔ Algebra.EssFiniteType (⊥ : Subfield F) F :=
diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean
index 1ba1ee31b36601..202202f7ca2440 100644
--- a/Mathlib/RingTheory/FiniteType.lean
+++ b/Mathlib/RingTheory/FiniteType.lean
@@ -202,6 +202,9 @@ lemma adjoin_of_finite {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} (h
   rw [← Subalgebra.fg_iff_finiteType]
   exact ⟨h.toFinset, by simp⟩
 
+instance {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} [Finite t] :
+    FiniteType R (Algebra.adjoin R t) := adjoin_of_finite t.toFinite
+
 end FiniteType
 
 end Algebra

From adb560534d38873a0ddbd017195bcce0ec78b76e Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 13:23:07 -0400
Subject: [PATCH 27/32] remove redundant `have`

---
 Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
index 467724c83aa967..d9e76329ff3dda 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
@@ -93,7 +93,6 @@ lemma fg_top_iff :
     (⊤ : IntermediateField F E).FG ↔ Algebra.EssFiniteType F E := by
   constructor
   · intro ⟨s, hs⟩
-    have : Algebra.FiniteType F (Algebra.adjoin F (s : Set E)) := .adjoin_of_finite s.finite_toSet
     have : Algebra.EssFiniteType (Algebra.adjoin F (s : Set E)) (adjoin F (s : Set E)) :=
       .of_isLocalization _ (nonZeroDivisors _)
     have : Algebra.EssFiniteType F (adjoin F (s : Set E)) :=

From 3658bfc50787c0285bbe003d3605d526e98384a4 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 14:11:06 -0400
Subject: [PATCH 28/32] make `K` and `L` explicit

---
 Mathlib/FieldTheory/FinTrdeg.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/FieldTheory/FinTrdeg.lean b/Mathlib/FieldTheory/FinTrdeg.lean
index 310b323fdb7f34..e4a0690205b392 100644
--- a/Mathlib/FieldTheory/FinTrdeg.lean
+++ b/Mathlib/FieldTheory/FinTrdeg.lean
@@ -83,6 +83,7 @@ theorem FinTrdeg.of_isTranscendenceBasis {ι : Type*} [Finite ι] {x : ι → L}
     ← hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0]
   exact Cardinal.mk_lt_aleph0
 
+variable (K L) in
 theorem exists_finset_isTranscendenceBasis [FinTrdeg K L] :
     ∃ s : Finset L, IsTranscendenceBasis K ((↑) : s → L) := by
   obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L

From 49a60d4b86d553daa107bbc491abe51e4941ae48 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 14:54:08 -0400
Subject: [PATCH 29/32] fix binder infos

---
 Mathlib/FieldTheory/FinTrdeg.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/FieldTheory/FinTrdeg.lean b/Mathlib/FieldTheory/FinTrdeg.lean
index e4a0690205b392..ee0c7d64506441 100644
--- a/Mathlib/FieldTheory/FinTrdeg.lean
+++ b/Mathlib/FieldTheory/FinTrdeg.lean
@@ -19,15 +19,14 @@ Equivalently, if L is an algebraic extension of a finitely generated field exten
 
 public section
 
-variable {K L : Type*} [Field K] [Field L] [Algebra K L]
-
 open IntermediateField
 
-variable (K L) in
 /-- A field extension L/K is said to have finite transcendence degree if there is some
 intermediate extension L/E/K with E/K finitely generated and L/E algebraic. -/
-class FinTrdeg where
-  exists_fg_isAlgebraic : ∃ E : IntermediateField K L, E.FG ∧ Algebra.IsAlgebraic E L
+class FinTrdeg (K L : Type*) [Field K] [Field L] [Algebra K L] where
+  exists_fg_isAlgebraic (K L) : ∃ E : IntermediateField K L, E.FG ∧ Algebra.IsAlgebraic E L
+
+variable {K L : Type*} [Field K] [Field L] [Algebra K L]
 
 variable (K L) in
 instance [Algebra.IsAlgebraic K L] : FinTrdeg K L where

From 9dc59cfd804c92538e2ab210e3b33b3966d10f35 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 15:08:56 -0400
Subject: [PATCH 30/32] more more instances

---
 Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean     | 4 ++++
 .../RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
index e29255c21b390a..6ca6ff097ed6f2 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
@@ -581,6 +581,10 @@ theorem finiteDimensional_adjoin {S : Set L} [Finite S] (hS : ∀ x ∈ S, IsInt
   have (x : S) := adjoin.finiteDimensional (hS x.1 x.2)
   exact finiteDimensional_iSup_of_finite
 
+instance {S : Set L} [Finite S] [Algebra.IsIntegral K L] :
+    FiniteDimensional K (adjoin K S) :=
+  finiteDimensional_adjoin fun _ _ => Algebra.IsIntegral.isIntegral _
+
 end PowerBasis
 
 /-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots
diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
index 4d82e9594a1417..8c749507e60e32 100644
--- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
+++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
@@ -142,6 +142,12 @@ theorem Algebra.IsIntegral.adjoin {S : Set A} (hS : ∀ x ∈ S, IsIntegral R x)
     Algebra.IsIntegral R (adjoin R S) :=
   le_integralClosure_iff_isIntegral.mp <| adjoin_le hS
 
+instance [Algebra.IsIntegral R A] (S : Set A) : Algebra.IsIntegral R (Algebra.adjoin R S) :=
+  Algebra.IsIntegral.adjoin fun _ _ => Algebra.IsIntegral.isIntegral _
+
+instance [Algebra.IsIntegral R A] (S : Set A) [Finite S] : Module.Finite R (Algebra.adjoin R S) :=
+  Algebra.IsIntegral.finite
+
 theorem integralClosure_eq_top_iff : integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A := by
   rw [← top_le_iff, le_integralClosure_iff_isIntegral,
       (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff] -- explicit arguments for speedup

From 1e0dab9369e6b1b96d371ce2112dfcf3b991ac66 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 20:00:55 -0400
Subject: [PATCH 31/32] progress

---
 Mathlib/FieldTheory/KrullTopology.lean | 183 +++++++++++++++----------
 1 file changed, 112 insertions(+), 71 deletions(-)

diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean
index 3ed9d6026c3be4..17367d26a15e79 100644
--- a/Mathlib/FieldTheory/KrullTopology.lean
+++ b/Mathlib/FieldTheory/KrullTopology.lean
@@ -5,8 +5,9 @@ Authors: Sebastian Monnet, Aaron Liu
 -/
 module
 
+public import Mathlib.FieldTheory.FinTrdeg
 public import Mathlib.FieldTheory.Galois.Basic
-public import Mathlib.Topology.Algebra.IsUniformGroup.Defs
+public import Mathlib.Topology.Algebra.IsUniformGroup.Basic
 -- this `import` is only used in the deprecated material at the bottom of the file
 -- it should be removed when the deprecated material is removed
 public import Mathlib.Topology.Algebra.FilterBasis
@@ -81,6 +82,27 @@ theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} :
   rw [Set.mem_iInter₂]
   rfl
 
+open SetRel IntermediateField in
+theorem krullTopology_mem_uniformity_iff_fg {s : SetRel Gal(L/K) Gal(L/K)} :
+    s ∈ 𝓤 Gal(L/K) ↔ ∃ F : IntermediateField K L,
+    F.FG ∧ ∀ σ τ : Gal(L/K), Set.EqOn σ τ F → σ ~[s] τ := by
+  rw [krullTopology_mem_uniformity_iff]
+  simp_rw [FG, existsAndEq, true_and]
+  refine exists_congr fun u => forall_congr' fun σ => forall_congr' fun τ => imp_congr_left ?_
+  unfold Set.EqOn
+  simp_rw [← AlgEquiv.symm_apply_eq, ← AlgEquiv.coe_inv, ← AlgEquiv.mul_apply]
+  have hst (σ : Gal(L/K)) (x : L) : σ x = x ↔ x ∈ fixedField (Subgroup.zpowers σ) := by
+    rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← adjoin_le_iff, le_iff_le,
+      Subgroup.zpowers_le, ← AlgEquiv.smul_def, ← MulAction.mem_stabilizer_iff]
+    revert σ
+    rw [← SetLike.ext_iff, le_antisymm_iff, ← le_iff_le, adjoin_simple_le_iff]
+    constructor
+    · simp
+    · intro σ hσ
+      simpa using hσ ⟨x, mem_adjoin_simple_self K x⟩
+  simp_rw [hst, ← Set.ofPred_subset_ofPred, SetLike.setOfPred_mem_eq,
+    Set.ofPred_mem_eq, SetLike.coe_subset_coe, adjoin_le_iff]
+
 variable (K L) in
 /-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on
 `Gal(L/K)` induced by the uniform structure. -/
@@ -116,29 +138,6 @@ instance : IsLeftUniformGroup Gal(L/K) where
     refine iInf_congr fun x => ?_
     simp [AlgEquiv.eq_symm_apply]
 
--- open IntermediateField in
--- variable (K L) in
--- /-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/
--- @[stacks 0BMJ "We define the Krull topology directly without proving the universal property"]
--- instance : IsUniformGroup Gal(L/K) where
---   uniformContinuous_div s hs := by
---     rw [krullTopology_mem_uniformity_iff] at hs
---     obtain ⟨F, _, hF⟩ := hs
---     rw [uniformity_prod_eq_prod, map_map, mem_map, mem_prod_self_iff]
---     refine ⟨{p | Set.EqOn p.1 p.2 (normalClosure K F L)}, ?_, ?_⟩
---     · rw [krullTopology_mem_uniformity_iff]
---       exact ⟨_, inferInstance, fun _ _ h => h⟩
---     rw [Set.prod_subset_iff]
---     intro σ hσ τ hτ
---     simp only [Set.mem_preimage, Function.comp_apply]
---     refine hF _ _ fun x hx => ?_
---     simp only [div_eq_mul_inv, AlgEquiv.mul_apply, AlgEquiv.coe_inv]
---     have hn : τ.1.symm x ∈ normalClosure K F L := by
---       have h : (AlgHom.comp τ.1.symm (IsScalarTower.toAlgHom K F L)).fieldRange ≤
---           normalClosure K F L := AlgHom.fieldRange_le_normalClosure _
---       exact h (by simpa using hx)
---     rw [hσ hn, σ.2.injective.eq_iff, AlgEquiv.eq_symm_apply, ← hτ hn, τ.1.apply_symm_apply]
-
 open IntermediateField in
 open scoped Topology in
 lemma krullTopology_mem_nhds_one_iff' {s : Set Gal(L/K)} :
@@ -278,6 +277,86 @@ instance krullTopology_discreteUniformity_of_essFiniteType
   rw [SetLike.mem_coe, ← hpe]
   exact hp x hx
 
+open IntermediateField in
+theorem AlgEquiv.isComplete_fixingSubgroup (E : IntermediateField K L) [FinTrdeg E L] :
+    IsComplete (E.fixingSubgroup : Set Gal(L/K)) := by
+  intro f hf hfE
+  rw [cauchy_iff] at hf
+  obtain ⟨_, hf⟩ := hf
+  obtain ⟨_, ⟨u, rfl⟩, alg⟩ := FinTrdeg.exists_fg_isAlgebraic E L
+  replace hf (F : IntermediateField K L) (_ : F.FG) :
+      ∃ σ : Gal(L/K), ∀ᶠ τ : Gal(L/K) in f, Set.EqOn σ τ F := by
+    obtain ⟨t, hf, ht⟩ := hf {p | Set.EqOn p.1 p.2 F}
+      (krullTopology_mem_uniformity_iff_fg.2 ⟨F, ‹_›, fun _ _ h => h⟩)
+    obtain ⟨σ, hσ⟩ := Filter.nonempty_of_mem hf
+    exact ⟨σ, Filter.eventually_of_mem hf fun τ hτ => @ht (σ, τ) ⟨hσ, hτ⟩⟩
+  have h (x : L) : ∃ y, ∀ᶠ τ in f, y = τ x :=
+    (hf (adjoin K {x}) (fg_adjoin_of_finite (Set.finite_singleton _))).elim
+      fun σ hσ => ⟨σ x, hσ.mono fun τ hτ => hτ (mem_adjoin_simple_self K x)⟩
+  choose s hs using h
+  let σh : L →ₐ[E] L :=
+    { toFun := s
+      map_zero' := (hs 0).exists.elim fun _ h => by simp [h]
+      map_one' := (hs 1).exists.elim fun _ h => by simp [h]
+      commutes' x :=
+        ((hs x.1).and ((Filter.eventually_mem_principal _).filter_mono hfE)).exists.elim fun _ h =>
+          by simp [h.1, (mem_fixingSubgroup_iff _ _).1 h.2]
+      map_add' x y := by
+        obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x + y)))).exists
+        simp [hτ.1, hτ.2.1, hτ.2.2]
+      map_mul' x y := by
+        obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x * y)))).exists
+        simp [hτ.1, hτ.2.1, hτ.2.2] }
+  let σ : Gal(L/E) := .ofBijective σh <| by
+    refine ⟨σh.injective, fun x => ?_⟩
+    obtain ⟨su, hsu, hsuE⟩ :=
+      (((Filter.eventually_all_finite u.finite_toSet).2 fun y hy => hs y).and
+        ((Filter.eventually_mem_principal _).filter_mono hfE)).exists
+    let Eu : IntermediateField E L := adjoin E (u : Set L)
+    let suE : Gal(L/E) := E.fixingSubgroupEquiv ⟨su, hsuE⟩
+    have algm : Algebra.IsIntegral (Eu.map (suE : L →ₐ[E] L)) L := sorry
+    let mp : Polynomial (Eu.map (suE : L →ₐ[E] L)) := minpoly _ x
+    let p : Polynomial Eu := mp.map
+      ((IntermediateField.equivMap Eu (suE : L →ₐ[E] L)).symm : Eu.map (suE : L →ₐ[E] L) →+* Eu)
+    have hp0 : p ≠ 0 := by
+      unfold p
+      refine (Polynomial.map_ne_zero_iff ?_).mpr ?_
+      · apply AlgEquiv.injective
+      unfold mp
+      apply minpoly.ne_zero
+      apply Algebra.IsIntegral.isIntegral
+    let S : Set L := p.rootSet L
+    have hS : S.Finite := Polynomial.rootSet_finite _ _
+    obtain ⟨τ, hτ, hτE⟩ :=
+      (((Filter.eventually_all_finite (u.finite_toSet.union hS)).2
+        fun y hy => hs y).and ((Filter.eventually_mem_principal _).filter_mono hfE)).exists
+    suffices h : τ.symm x ∈ S from ⟨τ.symm x, by simp [hτ (τ.symm x) (Set.mem_union_right u h), σh]⟩
+    let τE : Gal(L/E) := E.fixingSubgroupEquiv ⟨τ, hτE⟩
+    have hττE : ⇑τ.symm = τE.symm := rfl
+    unfold S
+    rw [Polynomial.mem_rootSet_of_ne hp0]
+    unfold p
+    apply (τE : L →+* L).injective
+    rw [hττE, map_zero, Polynomial.aeval_def, Polynomial.hom_eval₂,
+      RingHom.coe_coe, τE.apply_symm_apply, Polynomial.eval₂_eq_eval_map, Polynomial.map_map]
+    stop
+    conv =>
+      enter [1, 2, 1]
+      equals τE.symm.toRingHom.comp (algebraMap _ _) => ext; simp [AlgEquiv.]
+    stop
+    sorry
+  refine ⟨E.fixingSubgroupEquiv.symm σ, (E.fixingSubgroupEquiv.symm σ).2, fun U hU => ?_⟩
+  rw [← map_mul_left_nhds_one, Filter.mem_map, krullTopology_mem_nhds_one_iff'] at hU
+  obtain ⟨F, fg, hF⟩ := hU
+  rw [← Set.image_subset_iff] at hF
+  refine Filter.mem_of_superset ?_ hF
+  obtain ⟨σ', hσ'⟩ := hf F fg
+  have eq : Set.EqOn σ σ' F := fun x hx =>
+    ((hs x).and hσ').exists.elim fun _ h => h.1.trans (h.2 hx).symm
+  filter_upwards [hσ'] with τ hτ
+  refine ⟨_ * τ, (F.mem_fixingSubgroup_iff _).2 fun x hx => ?_, mul_inv_cancel_left _ τ⟩
+  simp [AlgEquiv.symm_apply_eq, eq hx, hτ hx]
+
 theorem AlgEquiv.totallyBounded_fixingSubgroup
     (E : IntermediateField K L) [Algebra.IsAlgebraic E L] :
     TotallyBounded (E.fixingSubgroup : Set Gal(L/K)) := by
@@ -297,8 +376,7 @@ theorem AlgEquiv.totallyBounded_fixingSubgroup
   let xE : F := ⟨x, IntermediateField.mem_adjoin_of_mem E hx⟩
   have hf : f (Function.invFun f (f σE)) xE = f σE xE :=
     DFunLike.congr_fun (Function.invFun_eq ⟨σE, rfl⟩) xE
-  -- TODO: add API for `IntermediateField.fixingSubgroup`
-  simpa [f, σE, xE, IntermediateField.fixingSubgroupEquiv] using hf.symm
+  simpa [f, σE, xE] using hf.symm
 
 variable (K L) in
 theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :
@@ -306,54 +384,17 @@ theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] :
   rw [← Subgroup.coe_top, ← IntermediateField.fixingSubgroup_bot]
   exact AlgEquiv.totallyBounded_fixingSubgroup ⊥
 
+variable (K L) in
+instance [FinTrdeg K L] : LocallyCompactSpace Gal(L/K) := sorry
+
+variable (K L) in
+instance [FinTrdeg K L] : CompleteSpace Gal(L/K) :=
+  IsLeftUniformGroup.completeSpace_of_weaklyLocallyCompactSpace
+
 variable (K L) in
 open IntermediateField in
 instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K) where
-  isCompact_univ := by
-    stop
-    apply (AlgEquiv.totallyBounded_univ K L).isCompact_of_isComplete
-    intro f hf _
-    rw [cauchy_iff] at hf
-    obtain ⟨_, hf⟩ := hf
-    replace hf (F : IntermediateField K L) (_ : FiniteDimensional K F) :
-        ∃ σ : Gal(L/K), ∀ᶠ τ : Gal(L/K) in f, Set.EqOn σ τ F := by
-      obtain ⟨t, hf, ht⟩ := hf {p | Set.EqOn p.1 p.2 F}
-        (krullTopology_mem_uniformity_iff.2 ⟨F, ‹_›, fun _ _ h => h⟩)
-      obtain ⟨σ, hσ⟩ := Filter.nonempty_of_mem hf
-      exact ⟨σ, Filter.eventually_of_mem hf fun τ hτ => @ht (σ, τ) ⟨hσ, hτ⟩⟩
-    have h (x : L) : ∃ y, ∀ᶠ τ in f, y = τ x :=
-      (hf (adjoin K {x}) (adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x))).elim
-        fun σ hσ => ⟨σ x, hσ.mono fun τ hτ => hτ (mem_adjoin_simple_self K x)⟩
-    choose s hs using h
-    let σ : Gal(L/K) := .ofBijective
-      { toFun := s
-        map_zero' := (hs 0).exists.elim fun _ h => by simp [h]
-        map_one' := (hs 1).exists.elim fun _ h => by simp [h]
-        commutes' x := (hs (algebraMap K L x)).exists.elim fun _ h => by simp [h]
-        map_add' x y := by
-          obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x + y)))).exists
-          simp [hτ.1, hτ.2.1, hτ.2.2]
-        map_mul' x y := by
-          obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x * y)))).exists
-          simp [hτ.1, hτ.2.1, hτ.2.2] } <| by
-      refine ⟨RingHom.injective _, fun x => ?_⟩
-      obtain ⟨τ, hτ⟩ :=
-        ((Filter.eventually_all_finite ((minpoly K x).rootSet_finite L)).2
-          fun y hy => hs y).exists
-      suffices h : τ.symm x ∈ (minpoly K x).rootSet L from ⟨τ.symm x, by simp [hτ (τ.symm x) h]⟩
-      rw [Polynomial.mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)),
-        Polynomial.aeval_algEquiv, AlgHom.comp_apply, minpoly.aeval, map_zero]
-    refine ⟨σ, Set.mem_univ σ, fun U hU => ?_⟩
-    rw [← map_mul_left_nhds_one, Filter.mem_map, krullTopology_mem_nhds_one_iff] at hU
-    obtain ⟨F, _, hF⟩ := hU
-    rw [← Set.image_subset_iff] at hF
-    refine Filter.mem_of_superset ?_ hF
-    obtain ⟨σ', hσ'⟩ := hf F ‹_›
-    have eq : Set.EqOn σ σ' F := fun x hx =>
-      ((hs x).and hσ').exists.elim fun _ h => h.1.trans (h.2 hx).symm
-    filter_upwards [hσ'] with τ hτ using
-      ⟨_, (F.mem_fixingSubgroup_iff _).2 fun x hx =>
-        by simp [AlgEquiv.symm_apply_eq, eq hx, hτ hx], mul_inv_cancel_left σ τ⟩
+  isCompact_univ := (AlgEquiv.totallyBounded_univ K L).isCompact_of_isComplete isComplete_univ
 
 section MulAction
 

From 36cf7477a1cdcfb50deb1a5afbd36a870c145427 Mon Sep 17 00:00:00 2001
From: Aaron Liu <aaronliu2008@outlook.com>
Date: Mon, 27 Jul 2026 20:03:41 -0400
Subject: [PATCH 32/32] deprecate

---
 Mathlib/Analysis/Calculus/FDeriv/Measurable.lean | 6 +++---
 Mathlib/NumberTheory/Padics/ProperSpace.lean     | 2 +-
 Mathlib/Topology/UniformSpace/Cauchy.lean        | 6 ++++--
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
index ff064c774c6fe5..305bb401e14bca 100644
--- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
+++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
@@ -372,7 +372,7 @@ variable [CompleteSpace F]
 /-- The set of differentiability points of a function taking values in a complete space is
 Borel-measurable. -/
 theorem measurableSet_of_differentiableAt : MeasurableSet { x | DifferentiableAt 𝕜 f x } := by
-  have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
+  have : IsComplete (univ : Set (E →L[𝕜] F)) := isComplete_univ
   convert! measurableSet_of_differentiableAt_of_isComplete 𝕜 f this
   simp
 
@@ -700,7 +700,7 @@ variable [CompleteSpace F]
 Borel-measurable. -/
 theorem measurableSet_of_differentiableWithinAt_Ici :
     MeasurableSet { x | DifferentiableWithinAt ℝ f (Ici x) x } := by
-  have : IsComplete (univ : Set F) := complete_univ
+  have : IsComplete (univ : Set F) := isComplete_univ
   convert! measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this
   simp
 
@@ -893,7 +893,7 @@ variable [CompleteSpace F]
 values in a complete space is Borel-measurable. -/
 theorem measurableSet_of_differentiableAt_with_param (hf : Continuous f.uncurry) :
     MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2} := by
-  have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
+  have : IsComplete (univ : Set (E →L[𝕜] F)) := isComplete_univ
   convert! measurableSet_of_differentiableAt_of_isComplete_with_param hf this
   simp
 
diff --git a/Mathlib/NumberTheory/Padics/ProperSpace.lean b/Mathlib/NumberTheory/Padics/ProperSpace.lean
index db68867d9bb6f2..2fe8af00160a22 100644
--- a/Mathlib/NumberTheory/Padics/ProperSpace.lean
+++ b/Mathlib/NumberTheory/Padics/ProperSpace.lean
@@ -54,7 +54,7 @@ theorem totallyBounded_univ : TotallyBounded (Set.univ : Set ℤ_[p]) := by
 /-- The set of p-adic integers `ℤ_[p]` is a compact topological space. -/
 instance compactSpace : CompactSpace ℤ_[p] := by
   rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete]
-  exact ⟨totallyBounded_univ p, complete_univ⟩
+  exact ⟨totallyBounded_univ p, isComplete_univ⟩
 
 end PadicInt
 
diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean
index e32c38af6b5a53..146088998669cd 100644
--- a/Mathlib/Topology/UniformSpace/Cauchy.lean
+++ b/Mathlib/Topology/UniformSpace/Cauchy.lean
@@ -371,11 +371,13 @@ class CompleteSpace (α : Type u) [UniformSpace α] : Prop where
   /-- In a complete uniform space, every Cauchy filter converges. -/
   complete : ∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ 𝓝 x
 
-theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] :
+theorem isComplete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] :
     IsComplete (univ : Set α) := fun f hf _ => by
   rcases CompleteSpace.complete hf with ⟨x, hx⟩
   exact ⟨x, mem_univ x, hx⟩
 
+@[deprecated (since := "2026-07-27")] alias complete_univ := isComplete_univ
+
 instance CompleteSpace.prod [UniformSpace β] [CompleteSpace α] [CompleteSpace β] :
     CompleteSpace (α × β) where
   complete hf :=
@@ -413,7 +415,7 @@ theorem completeSpace_of_isComplete_univ (h : IsComplete (univ : Set α)) : Comp
   ⟨fun hf => let ⟨x, _, hx⟩ := h _ hf ((@principal_univ α).symm ▸ le_top); ⟨x, hx⟩⟩
 
 theorem completeSpace_iff_isComplete_univ : CompleteSpace α ↔ IsComplete (univ : Set α) :=
-  ⟨@complete_univ α _, completeSpace_of_isComplete_univ⟩
+  ⟨@isComplete_univ α _, completeSpace_of_isComplete_univ⟩
 
 theorem completeSpace_iff_ultrafilter :
     CompleteSpace α ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ∃ x : α, ↑l ≤ 𝓝 x := by