diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
index a2651f5..08008a1 100644
--- a/FltRegular/NumberTheory/Hilbert92.lean
+++ b/FltRegular/NumberTheory/Hilbert92.lean
@@ -288,14 +288,13 @@ def relativeUnitsMapHom : (K →ₐ[k] K) →* (Monoid.End (RelativeUnits k K))
     obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
     rw [relativeUnitsMap]
     erw [QuotientGroup.lift_mk']
-    simp only [map_one, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply,
-      Monoid.coe_one, id_eq]
+    simp only [map_one, MonoidHom.coe_comp, QuotientGroup.coe_mk', Function.comp_apply]
     rfl
   map_mul' := by
     intros f g
     refine DFunLike.ext _ _ (fun x ↦ ?_)
     obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
-    simp only [relativeUnitsMap, map_mul, Monoid.coe_mul, Function.comp_apply]
+    simp only [relativeUnitsMap, map_mul, Function.comp_apply]
     rfl
 
 @[simps! apply]
diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean
index 727d1ba..5900837 100644
--- a/FltRegular/NumberTheory/Hilbert94.lean
+++ b/FltRegular/NumberTheory/Hilbert94.lean
@@ -131,7 +131,7 @@ theorem dvd_card_classGroup_of_isUnramified_isCyclic (K L : Type*)
     finrank K L ∣ Fintype.card (ClassGroup (𝓞 K)) := by
   obtain ⟨I, hI, hI'⟩ := exists_not_isPrincipal_and_isPrincipal_map K L hKL hKL'
   letI := Fact.mk hKL
-  rw [← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hKL).irreducible.dvd_iff_not_coprime,
+  rw [← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hKL).irreducible.dvd_iff_not_isCoprime,
     Nat.isCoprime_iff_coprime]
   exact fun h ↦ hI (IsPrincipal_of_IsPrincipal_pow_of_Coprime _ _ h _
     (Ideal.isPrincipal_pow_finrank_of_isPrincipal_map _ hI'))
diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean
index 084d290..7fcd21a 100644
--- a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean
+++ b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean
@@ -39,7 +39,7 @@ theorem not_for_all_zeta_sub_one_pow_dvd_sub_one_of_pow_ne (u : (𝓞 K)ˣ)
   have := KummersLemma.isUnramified hp hζ u hcong hu L
   have := dvd_card_classGroup_of_isUnramified_isCyclic K L (hKL.symm ▸ hpri.out)
     (hKL.symm ▸ PNat.coe_injective.ne hp)
-  rw [hKL, ← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hpri.out).irreducible.dvd_iff_not_coprime,
+  rw [hKL, ← Int.ofNat_dvd, (Nat.prime_iff_prime_int.mp hpri.out).irreducible.dvd_iff_not_isCoprime,
     Nat.isCoprime_iff_coprime] at this
   exact this (by convert hreg)
 
diff --git a/lake-manifest.json b/lake-manifest.json
index da7e752..3c5312d 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8c60540fe18528a8a857d4d88094b005af61d97b",
+   "rev": "e9d995eaa95a4e3c880ffe94c416c34113e0f251",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f68a59e8c389d12bafbaf4fada2bfc33c37105f2",
+   "rev": "b632e4bf07f6be125b1fc831b70c479d15860c71",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,