From b5bd4dd906cd135418390f87ffed6e13415d7b0f Mon Sep 17 00:00:00 2001
From: jjdishere <emailboxofjjd@163.com>
Date: Wed, 23 Oct 2024 19:13:09 +0200
Subject: [PATCH] remove covered import

move lemmas

typo

fix large import
---
 Mathlib/FieldTheory/Adjoin.lean               | 71 ---------------
 .../FieldTheory/IntermediateField/Basic.lean  | 87 +++++++++++++++++++
 Mathlib/Topology/Algebra/Field.lean           |  3 +-
 3 files changed, 88 insertions(+), 73 deletions(-)

diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
index f5504ce434121..bea1a6cc6ae43 100644
--- a/Mathlib/FieldTheory/Adjoin.lean
+++ b/Mathlib/FieldTheory/Adjoin.lean
@@ -89,9 +89,6 @@ def gi : GaloisInsertion (adjoin F : Set E → IntermediateField F E)
 
 instance : CompleteLattice (IntermediateField F E) where
   __ := GaloisInsertion.liftCompleteLattice IntermediateField.gi
-  bot :=
-    { toSubalgebra := ⊥
-      inv_mem' := by rintro x ⟨r, rfl⟩; exact ⟨r⁻¹, map_inv₀ _ _⟩ }
   bot_le x := (bot_le : ⊥ ≤ x.toSubalgebra)
 
 theorem sup_def (S T : IntermediateField F E) : S ⊔ T = adjoin F (S ∪ T : Set E) := rfl
@@ -106,33 +103,6 @@ instance : Unique (IntermediateField F F) :=
   { inferInstanceAs (Inhabited (IntermediateField F F)) with
     uniq := fun _ ↦ toSubalgebra_injective <| Subsingleton.elim _ _ }
 
-theorem coe_bot : ↑(⊥ : IntermediateField F E) = Set.range (algebraMap F E) := rfl
-
-theorem mem_bot {x : E} : x ∈ (⊥ : IntermediateField F E) ↔ x ∈ Set.range (algebraMap F E) :=
-  Iff.rfl
-
-@[simp]
-theorem bot_toSubalgebra : (⊥ : IntermediateField F E).toSubalgebra = ⊥ := rfl
-
-theorem bot_toSubfield : (⊥ : IntermediateField F E).toSubfield = (algebraMap F E).fieldRange :=
-  rfl
-
-@[simp]
-theorem coe_top : ↑(⊤ : IntermediateField F E) = (Set.univ : Set E) :=
-  rfl
-
-@[simp]
-theorem mem_top {x : E} : x ∈ (⊤ : IntermediateField F E) :=
-  trivial
-
-@[simp]
-theorem top_toSubalgebra : (⊤ : IntermediateField F E).toSubalgebra = ⊤ :=
-  rfl
-
-@[simp]
-theorem top_toSubfield : (⊤ : IntermediateField F E).toSubfield = ⊤ :=
-  rfl
-
 @[simp, norm_cast]
 theorem coe_inf (S T : IntermediateField F E) : (↑(S ⊓ T) : Set E) = (S : Set E) ∩ T :=
   rfl
@@ -229,47 +199,6 @@ theorem equivOfEq_trans {S T U : IntermediateField F E} (hST : S = T) (hTU : T =
     (equivOfEq hST).trans (equivOfEq hTU) = equivOfEq (hST.trans hTU) :=
   rfl
 
-variable (F E)
-
-/-- The bottom intermediate_field is isomorphic to the field. -/
-noncomputable def botEquiv : (⊥ : IntermediateField F E) ≃ₐ[F] F :=
-  (Subalgebra.equivOfEq _ _ bot_toSubalgebra).trans (Algebra.botEquiv F E)
-
-variable {F E}
-
--- Porting note: this was tagged `simp`.
-theorem botEquiv_def (x : F) : botEquiv F E (algebraMap F (⊥ : IntermediateField F E) x) = x := by
-  simp
-
-@[simp]
-theorem botEquiv_symm (x : F) : (botEquiv F E).symm x = algebraMap F _ x :=
-  rfl
-
-noncomputable instance algebraOverBot : Algebra (⊥ : IntermediateField F E) F :=
-  (IntermediateField.botEquiv F E).toAlgHom.toRingHom.toAlgebra
-
-theorem coe_algebraMap_over_bot :
-    (algebraMap (⊥ : IntermediateField F E) F : (⊥ : IntermediateField F E) → F) =
-      IntermediateField.botEquiv F E :=
-  rfl
-
-instance isScalarTower_over_bot : IsScalarTower (⊥ : IntermediateField F E) F E :=
-  IsScalarTower.of_algebraMap_eq
-    (by
-      intro x
-      obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x
-      rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
-        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E])
-
-/-- The top `IntermediateField` is isomorphic to the field.
-
-This is the intermediate field version of `Subalgebra.topEquiv`. -/
-@[simps!]
-def topEquiv : (⊤ : IntermediateField F E) ≃ₐ[F] E :=
-  Subalgebra.topEquiv
-
--- Porting note: this theorem is now generated by the `@[simps!]` above.
-
 section RestrictScalars
 
 @[simp]
diff --git a/Mathlib/FieldTheory/IntermediateField/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Basic.lean
index a5bccbb4de0b8..5d371afd906e2 100644
--- a/Mathlib/FieldTheory/IntermediateField/Basic.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Basic.lean
@@ -798,4 +798,91 @@ end Restrict
 
 end Tower
 
+section Bot
+
+instance instBot : Bot (IntermediateField K L) :=
+  ⟨{ (⊥ : Subalgebra K L) with
+    inv_mem' := by rintro x ⟨r, rfl⟩; exact ⟨r⁻¹, map_inv₀ _ _⟩,
+    }⟩
+
+theorem coe_bot : ↑(⊥ : IntermediateField K L) = Set.range (algebraMap K L) := rfl
+
+theorem mem_bot {x : L} : x ∈ (⊥ : IntermediateField K L) ↔ x ∈ Set.range (algebraMap K L) :=
+  Iff.rfl
+
+@[simp]
+theorem bot_toSubalgebra : (⊥ : IntermediateField K L).toSubalgebra = ⊥ := rfl
+
+theorem bot_toSubfield : (⊥ : IntermediateField K L).toSubfield = (algebraMap K L).fieldRange :=
+  rfl
+
+variable (K L)
+/-- The bottom intermediate_field is isomorphic to the field. -/
+noncomputable def botEquiv : (⊥ : IntermediateField K L) ≃ₐ[K] K :=
+  (Subalgebra.equivOfEq _ _ bot_toSubalgebra).trans (Algebra.botEquiv K L)
+
+variable {K L}
+
+-- Porting note: this was tagged `simp`.
+theorem botEquiv_def (x : K) : botEquiv K L (algebraMap K (⊥ : IntermediateField K L) x) = x := by
+  simp
+
+@[simp]
+theorem botEquiv_symm (x : K) : (botEquiv K L).symm x = algebraMap K _ x :=
+  rfl
+
+noncomputable instance algebraOverBot : Algebra (⊥ : IntermediateField K L) K :=
+  (IntermediateField.botEquiv K L).toAlgHom.toRingHom.toAlgebra
+
+theorem coe_algebraMap_over_bot :
+    (algebraMap (⊥ : IntermediateField K L) K : (⊥ : IntermediateField K L) → K) =
+      IntermediateField.botEquiv K L :=
+  rfl
+
+instance isScalarTower_over_bot : IsScalarTower (⊥ : IntermediateField K L) K L :=
+  IsScalarTower.of_algebraMap_eq
+    (by
+      intro x
+      obtain ⟨y, rfl⟩ := (botEquiv K L).symm.surjective x
+      rw [coe_algebraMap_over_bot, (botEquiv K L).apply_symm_apply, botEquiv_symm,
+        IsScalarTower.algebraMap_apply K (⊥ : IntermediateField K L) L])
+
+end Bot
+
+section Top
+
+instance instTop : Top (IntermediateField K L) :=
+  ⟨{ (⊤ : Subalgebra K L) with
+    inv_mem' := by tauto
+    }⟩
+
+@[simp]
+theorem coe_top : ↑(⊤ : IntermediateField K L) = (Set.univ : Set L) :=
+  rfl
+
+@[simp]
+theorem mem_top {x : L} : x ∈ (⊤ : IntermediateField K L) :=
+  trivial
+
+@[simp]
+theorem top_toSubalgebra : (⊤ : IntermediateField K L).toSubalgebra = ⊤ :=
+  rfl
+
+@[simp]
+theorem top_toSubfield : (⊤ : IntermediateField K L).toSubfield = ⊤ :=
+  rfl
+
+variable (K L)
+
+/-- The top `IntermediateField` is isomorphic to the field.
+
+This is the intermediate field version of `Subalgebra.topEquiv`. -/
+@[simps!]
+def topEquiv : (⊤ : IntermediateField K L) ≃ₐ[K] L :=
+  Subalgebra.topEquiv
+
+-- Porting note: this theorem is now generated by the `@[simps!]` above.
+
+end Top
+
 end IntermediateField
diff --git a/Mathlib/Topology/Algebra/Field.lean b/Mathlib/Topology/Algebra/Field.lean
index 9e6b964c7d50a..ec8b45984d12f 100644
--- a/Mathlib/Topology/Algebra/Field.lean
+++ b/Mathlib/Topology/Algebra/Field.lean
@@ -3,8 +3,7 @@ Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Kim Morrison
 -/
-import Mathlib.FieldTheory.Adjoin
-import Mathlib.Algebra.GroupWithZero.Divisibility
+import Mathlib.FieldTheory.IntermediateField.Basic
 import Mathlib.Topology.Algebra.GroupWithZero
 import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Order.LocalExtr