diff --git a/GaloisRamification/GaloisRamification.lean b/GaloisRamification/GaloisRamification.lean
index 91739c2..2dbe604 100644
--- a/GaloisRamification/GaloisRamification.lean
+++ b/GaloisRamification/GaloisRamification.lean
@@ -89,34 +89,6 @@ theorem prime_iff_isMaximal {p : Ideal A} (hp0 : p ≠ ⊥) : Prime p ↔ p.IsMa
   ⟨fun hp ↦ (isPrime_of_prime hp).isMaximal hp.ne_zero,
     fun hp ↦ prime_of_isPrime hp0 hp.isPrime⟩
 
-namespace Ideal
--- lemmas of isomorphisms act on ideals
-/-- A ring isomorphism sends a prime ideal to a prime ideal. -/
-instance {R S E : Type*} [CommRing R] [CommRing S] (p : Ideal R) [p.IsPrime] [EquivLike E R S]
-    [RingEquivClass E R S] (e : E) : (map e p).IsPrime := by
-  exact map_isPrime_of_equiv e
-
-/-- A ring isomorphism sends a maximal ideal to a maximal ideal. -/
-instance map_isMaximal_of_equiv {R S E : Type*} [Ring R] [Ring S] (p : Ideal R)
-    [hp : p.IsMaximal] [EquivLike E R S] [RingEquivClass E R S] (e : E) : (map e p).IsMaximal :=
-  map.isMaximal e (EquivLike.bijective e) hp
-
-/-- A maximal ideal pull back by a ring isomorphism is a maximal ideal. -/
-instance comap_isMaximal_of_equiv {R S E : Type*} [Ring R] [Ring S] (p : Ideal S)
-    [p.IsMaximal] [EquivLike E R S] [RingEquivClass E R S] (e : E) : (comap e p).IsMaximal :=
-  comap_isMaximal_of_surjective e (EquivLike.surjective e)
-
-theorem mem_map_of_equiv {R S E : Type*} [Semiring R] [Semiring S] (I : Ideal R)
-    [EquivLike E R S] [RingEquivClass E R S] (e : E) (y : S) : y ∈ map e I ↔ ∃ x ∈ I, e x = y := by
-  constructor
-  · intro h
-    simp_rw [show map e I = _ from map_comap_of_equiv I (e : R ≃+* S)] at h
-    exact ⟨(e : R ≃+* S).symm y, h, RingEquiv.apply_symm_apply (e : R ≃+* S) y⟩
-  · rintro ⟨x, hx, rfl⟩
-    exact mem_map_of_mem e hx
-
-end Ideal
-
 end lie_over
 
 section transitive
diff --git a/GaloisRamification/ToMathlib.lean b/GaloisRamification/ToMathlib.lean
index 5dd66b3..4101d89 100644
--- a/GaloisRamification/ToMathlib.lean
+++ b/GaloisRamification/ToMathlib.lean
@@ -9,6 +9,7 @@ import Mathlib.RingTheory.Valuation.ValuationRing
 
 import GaloisRamification.ToMathlib.Finite
 import GaloisRamification.ToMathlib.FractionRing
+import GaloisRamification.ToMathlib.IsGalois
 import GaloisRamification.ToMathlib.Normal
 import GaloisRamification.ToMathlib.restrictScalarsHom
 import GaloisRamification.ToMathlib.separableClosure
diff --git a/lake-manifest.json b/lake-manifest.json
index e16da4e..b9373cc 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
+   "rev": "85f6511d93f9e6a8188ec9985c82f08f65c26cae",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e91cdbcf5a387801a6225b41b0056c63206a9f7f",
+   "rev": "e43d3141c5d7f7a2db92205bb02f6fee3c7f9d75",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,