diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean
index fb235243..0a830c9c 100644
--- a/FltRegular/CaseI/Statement.lean
+++ b/FltRegular/CaseI/Statement.lean
@@ -98,21 +98,18 @@ variable (p)
 These instances are related to the problem described in
 https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/slowness.20in.20ring.20theory.20file
 -/
-instance foo1 : @IsDomain (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))
-  (@CommSemiring.toSemiring _ CommRing.toCommSemiring) :=
-inferInstance
 
 instance foo2 : IsDedekindDomain (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) :=
 inferInstance
 
 instance foo3 : @IsDomain (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))) CommSemiring.toSemiring := by
-  convert @Ideal.isDomain (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) _ (foo1 p) (foo2 p)
+  convert @Ideal.isDomain (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)) _ (foo2 p)
 
 noncomputable
 instance foo4 : @NormalizedGCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)))
   (@IsDomain.toCancelCommMonoidWithZero _ (@IdemCommSemiring.toCommSemiring _
     Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule) (foo3 p)) := by
-  convert @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero _ _ (foo1 p) (foo2 p)
+  convert @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero _ _ (foo2 p)
 
 noncomputable
 instance foo5 : @GCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)))
@@ -204,14 +201,14 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     simp only [Fin.val_mk, SubsemiringClass.coe_pow, NumberField.Units.coe_zpow,
       IsPrimitiveRoot.coe_unit'_coe]
     refine' eq_of_div_eq_one _
-    rw [← zpow_coe_nat, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
+    rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.int_cast_zmod_eq_zero_iff_dvd,
       Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, int_cast_ofNat, sub_self]
   · rw [← Subtype.coe_inj]
     simp only [Fin.val_mk, SubsemiringClass.coe_pow, MulMemClass.coe_mul,
       NumberField.Units.coe_zpow, IsPrimitiveRoot.coe_unit'_coe, IsPrimitiveRoot.coe_inv_unit'_coe]
     refine' eq_of_div_eq_one _
-    rw [← zpow_coe_nat, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
+    rw [← zpow_natCast, ← zpow_sub_one₀ (hζ'.ne_zero hpri.out.ne_zero), ←
       zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
     simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.int_cast_zmod_eq_zero_iff_dvd,
       Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, int_cast_ofNat, Int.cast_one, sub_self]
diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean
index c68c8382..20e65b52 100644
--- a/FltRegular/CaseII/AuxLemmas.lean
+++ b/FltRegular/CaseII/AuxLemmas.lean
@@ -35,7 +35,7 @@ lemma WfDvdMonoid.multiplicity_finite {M : Type*} [CancelCommMonoidWithZero M] [
     rw [hf (n + 1), e, mul_zero]
   · refine ⟨x, hx, ?_⟩
     rw [mul_comm, ← (mul_right_injective₀ (a := x ^ (n + 1)) _).eq_iff]
-    · simp only [← mul_assoc, ← pow_succ', ← hf]
+    · simp only [← mul_assoc, ← pow_succ, ← hf]
     · intro e
       apply hy
       rw [hf n, e, zero_mul]
@@ -187,7 +187,7 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
           rwa [e, ← dvd_gcd_mul_iff_dvd_mul, this, one_mul] at h
         obtain ⟨a', rfl⟩ := ha'
         obtain ⟨b', rfl⟩ := hb'
-        rw [pow_succ, mul_dvd_mul_iff_left hx.ne_zero] at ha hb
+        rw [pow_succ', mul_dvd_mul_iff_left hx.ne_zero] at ha hb
         rw [_root_.map_mul, _root_.map_mul, mul_div_mul_left] at e₀
         · exact IH ⟨a', b', ha, hb, e₀⟩
         · rw [Ne.def, ← (algebraMap R K).map_zero, (IsFractionRing.injective R K).eq_iff]
diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean
index b92d00c9..3d4364e8 100644
--- a/FltRegular/CaseII/InductionStep.lean
+++ b/FltRegular/CaseII/InductionStep.lean
@@ -60,7 +60,7 @@ lemma div_one_sub_zeta_mem : (x + y * η : 𝓞 K) / (ζ - 1) ∈ 𝓞 K := by
   rw [e, mul_comm]
   simp only [Submonoid.coe_mul, Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring,
     AddSubgroupClass.coe_sub, IsPrimitiveRoot.val_unit'_coe, OneMemClass.coe_one, ne_eq]
-  rwa [mul_div_cancel _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
+  rwa [mul_div_cancel_right₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 def div_zeta_sub_one : nthRootsFinset p (𝓞 K) → 𝓞 K :=
 fun η ↦ ⟨(x + y * η) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩
@@ -68,7 +68,7 @@ fun η ↦ ⟨(x + y * η) / (ζ - 1), div_one_sub_zeta_mem hp hζ e η⟩
 lemma div_zeta_sub_one_mul_zeta_sub_one (η) :
     div_zeta_sub_one hp hζ e η * (π) = x + y * η := by
   ext
-  simp [div_zeta_sub_one, div_mul_cancel _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
+  simp [div_zeta_sub_one, div_mul_cancel₀ _ (hζ.sub_one_ne_zero hpri.out.one_lt)]
 
 lemma div_zeta_sub_one_sub (η₁ η₂) (hη : η₁ ≠ η₂) :
     Associated y (div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂) := by
@@ -231,8 +231,8 @@ lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (
     exists_ideal_pow_eq_c_aux]
 
 lemma exists_ideal_pow_eq_c : ∃ I : Ideal (𝓞 K), (𝔠 η) = I ^ (p : ℕ) := by
-  letI inst1 : @IsDomain (Ideal (𝓞 K)) CommSemiring.toSemiring := @Ideal.isDomain (𝓞 K) _ _ _
-  letI inst2 := @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero (𝓞 K) _ _ _
+  letI inst1 : @IsDomain (Ideal (𝓞 K)) CommSemiring.toSemiring := @Ideal.isDomain (𝓞 K) _ _
+  letI inst2 := @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero (𝓞 K) _ _
   letI inst3 := @NormalizedGCDMonoid.toGCDMonoid _ _ inst2
   exact @Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (nthRootsFinset p (𝓞 K)) (Ideal (𝓞 K)) _
     (by convert inst1) (by convert inst3) _ _ _ _ _
@@ -547,5 +547,5 @@ lemma exists_solution' :
     exact ⟨b ^ (p : ℕ), this⟩
   refine ⟨ε' * x', y', z', ε₃ / ε₂, hy', hz', ?_⟩
   rwa [mul_pow, ← Units.val_pow_eq_pow_val, ← hε', ← mul_right_inj' ε₂.isUnit.ne_zero,
-    mul_add, ← mul_assoc, ← Units.val_mul, mul_div_cancel'_right,
-    ← mul_assoc, ← Units.val_mul, mul_div_cancel'_right]
+    mul_add, ← mul_assoc, ← Units.val_mul, mul_div_cancel,
+    ← mul_assoc, ← Units.val_mul, mul_div_cancel]
diff --git a/FltRegular/CaseII/Statement.lean b/FltRegular/CaseII/Statement.lean
index 5b0c0971..db433084 100644
--- a/FltRegular/CaseII/Statement.lean
+++ b/FltRegular/CaseII/Statement.lean
@@ -42,7 +42,7 @@ lemma not_exists_solution' :
         pow_one]
     · intro h'
       have := mul_dvd_mul_left (((hζ.unit' : 𝓞 K) - 1) ^ Part.get (multiplicity _ z) H) h'
-      rw [← pow_succ', ← h] at this
+      rw [← pow_succ, ← h] at this
       exact multiplicity.is_greatest' H (Nat.lt_succ_self _) this
   refine not_exists_solution hp hreg hζ hm ⟨x, y, z, 1, hy, hz'', ?_⟩
   rwa [Units.val_one, one_mul]
@@ -72,7 +72,7 @@ lemma not_exists_Int_solution' {p : ℕ} [hpri : Fact (Nat.Prime p)] (hreg : IsR
   refine not_exists_Int_solution hreg hodd ⟨x, y, z, ?_, hz, hz', e⟩
   intro hy
   have := dvd_sub (dvd_pow hz hpri.out.ne_zero) (dvd_pow hy hpri.out.ne_zero)
-  rw [← e, add_sub_cancel] at this
+  rw [← e, add_sub_cancel_right] at this
   replace this := (Nat.prime_iff_prime_int.mp hpri.out).dvd_of_dvd_pow this
   apply (Nat.prime_iff_prime_int.mp hpri.out).not_unit
   rw [isUnit_iff_dvd_one, ← hgcd]
diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean
index 925ed08f..0acf2ec7 100644
--- a/FltRegular/FltThree/FltThree.lean
+++ b/FltRegular/FltThree/FltThree.lean
@@ -474,8 +474,7 @@ theorem gcd3_coprime {u v : ℤ} (huvcoprime : IsCoprime u v) (huvodd : Even u 
   by
   have haddodd : ¬Even (u + v) := by simp [huvodd, parity_simps]
   have hsubodd : ¬Even (u - v) := by simp [huvodd, parity_simps]
-  have haddcoprime : IsCoprime (u + v) (2 * v) :=
-    by
+  have haddcoprime : IsCoprime (u + v) (2 * v) := by
     apply isCoprime_of_prime_dvd
     · rintro ⟨h1, -⟩
       rw [h1] at haddodd
@@ -486,10 +485,8 @@ theorem gcd3_coprime {u v : ℤ} (huvcoprime : IsCoprime u v) (huvodd : Even u 
       rw [even_iff_two_dvd] at haddodd
       exact Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two hkdvdright
     apply huvcoprime.isUnit_of_dvd' _ hkdvdright'
-    rw [← add_sub_cancel u v]
-    apply dvd_sub hkdvdleft hkdvdright'
-  have hsubcoprime : IsCoprime (u - v) (2 * v) :=
-    by
+    simpa using dvd_sub hkdvdleft hkdvdright'
+  have hsubcoprime : IsCoprime (u - v) (2 * v) := by
     apply isCoprime_of_prime_dvd
     · rintro ⟨h1, -⟩
       rw [h1] at hsubodd
@@ -502,8 +499,7 @@ theorem gcd3_coprime {u v : ℤ} (huvcoprime : IsCoprime u v) (huvodd : Even u 
     apply huvcoprime.isUnit_of_dvd' _ hkdvdright'
     rw [← sub_add_cancel u v]
     exact dvd_add hkdvdleft hkdvdright'
-  have haddsubcoprime : IsCoprime (u + v) (u - v) :=
-    by
+  have haddsubcoprime : IsCoprime (u + v) (u - v) := by
     apply isCoprime_of_prime_dvd
     · rintro ⟨h1, -⟩
       rw [h1] at haddodd
diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean
index 03fdebb8..eb3a1e98 100644
--- a/FltRegular/FltThree/Spts.lean
+++ b/FltRegular/FltThree/Spts.lean
@@ -401,7 +401,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs
       exact sq_pos_of_ne_zero _ hq
   refine' ⟨_, hq⟩
   calc
-    p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by rw [hq, mul_one, add_sub_cancel]
+    p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by simp [hq]
     _ = p.norm - 3 := by
       rw [Zsqrtd.norm_def]
       ring
diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
index 33711c85..3ac61395 100644
--- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -16,8 +16,6 @@ instance Ring.toSubtractionMonoid {S : Type*} [Ring S] : SubtractionMonoid S :=
 
 section IntFacts
 
-noncomputable section
-
 open scoped NumberField BigOperators
 
 instance {K : Type*} [Field K] : Module (𝓞 K) (𝓞 K) := Semiring.toModule
@@ -63,45 +61,13 @@ theorem exists_int_sub_pow_prime_dvd {A : Type _} [CommRing A] [IsCyclotomicExte
     congr 1
     exact (sub_eq_zero.mp hb).symm
 
-example {R A : Type _} [CommRing R] [CommRing A] [Algebra R A] [IsCyclotomicExtension {p} R A]
-    [Fact (p : ℕ).Prime] (a : A) :
-    ∃ m : R, a ^ (p : ℕ) - algebraMap R A m ∈ span ({(p : A)} : Set A) := by
-  by_cases hpunit : ↑(p : ℕ) ∈ nonunits A
-  swap
-  · simp only [mem_nonunits_iff, Classical.not_not] at hpunit
-    exact ⟨0, by simp [Ideal.span_singleton_eq_top.2 hpunit]⟩
-  have : a ∈ Algebra.adjoin R _ := @adjoin_roots {p} R A _ _ _ _ a
-  refine' Algebra.adjoin_induction this _ (fun r => ⟨r ^ (p : ℕ), by simp⟩) _ _
-  · rintro x ⟨hx_w, hx_m, hx_p⟩
-    simp only [Set.mem_singleton_iff] at hx_m
-    rw [hx_m] at hx_p
-    exact ⟨1, by simp [hx_p]⟩
-  · rintro x y ⟨b, hb⟩ ⟨c, hc⟩
-    use c + b
-    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero] at hb hc ⊢
-    haveI : CharP (A ⧸ span ({(p : A)} : Set A)) (p : ℕ) := by
-      convert CharP.quotient A (p : ℕ) hpunit
-    rw [map_add, map_pow, map_add, add_pow_char_of_commute (A ⧸ span ({(p : A)} : Set A)) _ _
-      (Commute.all _ _), ← map_pow, ← map_pow]
-    rw [hb, hc]
-    simp [add_comm]
-  · rintro x y ⟨b, hb⟩ ⟨c, hc⟩
-    rw [mul_pow]
-    use b * c
-    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero] at hb hc ⊢
-    simp only [_root_.map_mul, Quotient.mk_algebraMap, hb, hc]
-
-
-instance aaaa [Fact (p : ℕ).Prime] : IsCyclotomicExtension {p} ℤ (𝓞 L) :=
-  let _ := (zeta_spec p ℚ L).adjoin_isCyclotomicExtension ℤ
-  IsCyclotomicExtension.equiv {p} _ _ (zeta_spec p ℚ L).adjoinEquivRingOfIntegers'
-
 local notation "R" => 𝓞 (CyclotomicField p ℚ)
 
 -- TODO I (alex) am not sure whether this is better as ideal span,
 -- or fractional_ideal.span_singleton
 /-- The principal ideal generated by `x + y ζ^i` for integer `x` and `y` -/
 @[nolint unusedArguments]
+noncomputable
 def fltIdeals [Fact (p : ℕ).Prime] (x y : ℤ) {η : R} (_ : η ∈ nthRootsFinset p R) : Ideal R :=
   Ideal.span ({x + η * y} : Set R)
 
@@ -153,7 +119,8 @@ attribute [-instance] CharP.CharOne.subsingleton
 theorem nth_roots_prim [Fact (p : ℕ).Prime] {η : R} (hη : η ∈ nthRootsFinset p R) (hne1 : η ≠ 1) :
     IsPrimitiveRoot η p := by
   have hζ' := (zeta_spec p ℚ (CyclotomicField p ℚ)).unit'_coe
-  rw [nthRoots_one_eq_biUnion_primitiveRoots' hζ', @Finset.mem_biUnion _ _ (_) _ _ _] at hη
+  rw [nthRoots_one_eq_biUnion_primitiveRoots' hζ'] at hη
+  simp only [mem_biUnion] at hη
   obtain ⟨a, ha, h2⟩ := hη
   have ha2 : a = p := by
     rw [Nat.Prime.divisors (Fact.out : Nat.Prime p), mem_insert, mem_singleton] at ha
@@ -223,6 +190,7 @@ theorem diff_of_roots2 [Fact (p : ℕ).Prime] (ph : 5 ≤ p) {η₁ η₂ : R} (
   rw [Units.val_neg, neg_mul, ← hu]
   ring
 
+noncomputable
 instance : AddCommGroup R := AddCommGroupWithOne.toAddCommGroup
 
 set_option maxHeartbeats 300000 in
diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
index 8763b4c3..06d1ac2e 100644
--- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
@@ -110,9 +110,9 @@ lemma exists_dvd_pow_sub_Int_pow (a : 𝓞 K) : ∃ b : ℤ, ↑p ∣ a ^ (p : 
   rw [(Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow, ← sub_eq_add_neg, e,
     mul_pow, ← sub_eq_add_neg] at hr
   nth_rw 1 [← Nat.sub_add_cancel (n := p) (m := 1) hpri.out.one_lt.le] at hr
-  rw [pow_succ', ← hu, mul_assoc, mul_assoc] at hr
+  rw [pow_succ, ← hu, mul_assoc, mul_assoc] at hr
   use b, ↑u * ((hζ.unit' - 1 : 𝓞 K) * k ^ (p : ℕ)) - r
-  rw [mul_sub, hr, add_sub_cancel]
+  rw [mul_sub, hr, add_sub_cancel_right]
 
 lemma norm_dvd_iff {R : Type*} [CommRing R] [IsDomain R] [IsDedekindDomain R]
     [Infinite R] [Module.Free ℤ R] [Module.Finite ℤ R] (x : R) (hx : Prime (Algebra.norm ℤ x)) {y : ℤ} :
@@ -211,7 +211,7 @@ lemma zeta_sub_one_pow_dvd_norm_sub_pow (x : 𝓞 K) :
     convert this using 1; ring
   apply dvd_add
   · apply dvd_mul_of_dvd_left
-    rw [ht, ← mul_assoc, ← pow_succ, tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le]
+    rw [ht, ← mul_assoc, ← pow_succ', tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le]
     exact dvd_mul_right _ _
   · rw [ht, mul_pow, ← pow_mul, mul_assoc]
     apply dvd_mul_of_dvd_left
diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
index 4104f9c1..c12caddd 100644
--- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -239,7 +239,6 @@ theorem roots_of_unity_in_cyclo (hpo : Odd (p : ℕ)) (x : K)
   have H : ∃ (m : ℕ) (k : ℕ+), (⟨x, hx⟩ : R) = (-1) ^ (k : ℕ) * (hζ.unit' : K) ^ (m : ℕ) := by
     obtain ⟨l, hl, hhl⟩ := (_root_.isRoot_of_unity_iff hn0 _).1 hxu
     have hlp := roots_of_unity_in_cyclo_aux hl hx hhl hζ
-    simp only [IsRoot.def] at hhl
     have isPrimRoot : IsPrimitiveRoot (hζ.unit' : R) p := hζ.unit'_coe
     have hxl : (⟨x, hx⟩ : R) ^ l = 1 :=  by
       apply isRoot_of_unity_of_root_cyclotomic _ hhl
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
index 6014ce0c..8ddad6ea 100644
--- a/FltRegular/NumberTheory/Hilbert92.lean
+++ b/FltRegular/NumberTheory/Hilbert92.lean
@@ -486,7 +486,7 @@ lemma u_lemma2 (u v : (𝓞 K)ˣ) (hu : u = v / (σ v : K)) : (mkG u) = (1 - zet
   ext
   simp only [Units.val_mul, Units.coe_map, MonoidHom.coe_coe, Submonoid.coe_mul,
     Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, coe_galRestrictHom_apply, hu]
-  refine div_mul_cancel _ ?_
+  refine div_mul_cancel₀ _ ?_
   simp only [ne_eq, map_eq_zero, ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true]
 
 open multiplicity in
@@ -529,8 +529,8 @@ lemma exists_pow_smul_eq_and_not_dvd
   use n, f', funext hf', i
   intro hi
   have : (p : ℤ) ^ (n + 1) ∣ f i
-  · rw [hf', pow_succ', Nat.cast_pow]
-    exact mul_dvd_mul_left _ hi
+  · rw [hf', pow_succ, Nat.cast_pow]
+    exact _root_.mul_dvd_mul_left _ hi
   simp [hfi, padicValInt_dvd_iff' hp] at this
 
 lemma lh_pow_free_aux {M} [CommGroup M] [Module.Finite ℤ (Additive M)] (ζ : M)
@@ -545,7 +545,7 @@ lemma lh_pow_free_aux {M} [CommGroup M] [Module.Finite ℤ (Additive M)] (ζ : M
     (Function.ne_iff.mpr hf') p hp.ne_one
   simp_rw [hf', Pi.smul_apply, smul_assoc, ← smul_sum] at hf
   obtain ⟨a, ha⟩ := hk _ _ hf
-  rw [← zpow_coe_nat] at ha
+  rw [← zpow_natCast] at ha
   exact ⟨a, f', i, ha.symm, hi⟩
 
 lemma Fin.castSucc_ne_last {r : ℕ} (x : Fin r) : Fin.castSucc x ≠ Fin.last r := by
@@ -759,7 +759,7 @@ lemma Hilbert92ish_aux1 (n : ℕ) (H : Fin n → Additive (𝓞 K)ˣ) (ζ : (
   apply_fun ((↑) : (𝓞 k)ˣ → k) at ha
   simp only [toMul_sum, toMul_zsmul, Units.coe_prod, Submonoid.coe_finset_prod, hη,
     Subsemiring.coe_toSubmonoid, Subalgebra.coe_toSubsemiring, Units.coe_zpow, toMul_ofMul] at ha
-  rwa [← zpow_coe_nat, ← zpow_mul, mul_comm _ a, mul_inv_eq_one₀]
+  rwa [← zpow_natCast, ← zpow_mul, mul_comm _ a, mul_inv_eq_one₀]
   rw [← Units.coe_zpow]
   simp only [ne_eq, ZeroMemClass.coe_eq_zero, Units.ne_zero, not_false_eq_true]
 
@@ -774,7 +774,7 @@ lemma Hilbert92ish_aux2 (E : (𝓞 K)ˣ) (ζ : k) (hE : algebraMap k K ζ = E /
       rw [hE]
       simp
     | succ n ih =>
-      rw [pow_succ, AlgEquiv.mul_apply, ih, pow_succ]
+      rw [pow_succ', AlgEquiv.mul_apply, ih, pow_succ']
       simp only [inv_pow, map_mul, map_inv₀, map_pow, AlgEquiv.commutes]
       have h0 : (algebraMap k K) ζ ≠ 0 := fun h ↦ by simp [(map_eq_zero _).1 h] at hζ
       field_simp [h0]
@@ -852,7 +852,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
       RingOfInteger.coe_algebraMap_apply, RingOfIntegers.norm_apply_coe, Units.val_pow_eq_pow_val, SubmonoidClass.coe_pow, Units.val_neg]
     rw [← map_pow] at hE
     refine Hilbert92ish_aux2 p hp hKL σ hσ E _ hE ?_ hpodd
-    rw [← pow_mul, ← pow_succ']
+    rw [← pow_mul, ← pow_succ]
     apply (hζ.pow_eq_one_iff_dvd _).2
     cases h <;> simp only [Nat.zero_eq, pow_zero, zero_le, tsub_eq_zero_of_le,
       zero_add, pow_one, one_dvd, Nat.succ_sub_succ_eq_sub,
@@ -897,7 +897,7 @@ lemma Hilbert92ish (hpodd : (p : ℕ) ≠ 2) :
         conv_rhs at ha => rw [smul_comm β, ← smul_add]
         rw [smul_smul, smul_smul, ← add_smul, mul_comm _ α, hαβ, one_smul] at ha
         exact ⟨_, ha.symm⟩
-      have hζ'' := (hζ.pow (p ^ h.succ).pos (pow_succ' _ _)).map_of_injective
+      have hζ'' := (hζ.pow (p ^ h.succ).pos (pow_succ _ _)).map_of_injective
         (algebraMap k K).injective
       obtain ⟨ε'', hε''⟩ : ∃ ε'' : (𝓞 k)ˣ, E = Units.map (algebraMap (𝓞 k) (𝓞 K)).toMonoidHom ε''
       · rw [← hε', map_pow, eq_comm, ← mul_inv_eq_one, ← inv_pow, ← mul_pow] at NE_p_pow
diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean
index bf81a5a4..9f1cf6bc 100644
--- a/FltRegular/NumberTheory/Hilbert94.lean
+++ b/FltRegular/NumberTheory/Hilbert94.lean
@@ -38,7 +38,7 @@ lemma comap_span_galRestrict_eq_of_cyclic (β : B) (η : Bˣ) (hβ : η * (galRe
     simp only [Nat.zero_eq, pow_zero, AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe]
     exact Ideal.map_id _
   | succ n IH =>
-    simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ'] at IH ⊢
+    simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, pow_succ] at IH ⊢
     conv_lhs at IH => rw [← hβ, Ideal.map_map]
     exact IH
 
@@ -62,7 +62,7 @@ theorem exists_not_isPrincipal_and_isPrincipal_map_aux
     use a
     conv_rhs => enter [1]; rw [← hβ]
     rw [map_mul, ← AlgHom.coe_coe σ, ← algebraMap_galRestrictHom_apply A K L B σ a]
-    refine (mul_div_cancel _ ?_).symm
+    refine (mul_div_cancel_right₀ _ ?_).symm
     · rw [ne_eq, (injective_iff_map_eq_zero' _).mp (IsIntegralClosure.algebraMap_injective B A L),
         (injective_iff_map_eq_zero' _).mp (galRestrict A K L B σ).injective]
       exact a.isUnit.ne_zero
diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean
index 735b9a29..58d61035 100644
--- a/FltRegular/NumberTheory/KummersLemma/Field.lean
+++ b/FltRegular/NumberTheory/KummersLemma/Field.lean
@@ -23,7 +23,7 @@ lemma zeta_sub_one_pow_dvd_poly :
   rw [← dvd_sub_left (_root_.map_dvd C hcong), add_sub_assoc, C.map_sub (u : 𝓞 K), ← sub_add,
     sub_self, map_one, zero_add]
   refine dvd_C_mul_X_sub_one_pow_add_one hpri.out (PNat.coe_injective.ne hp) _ _ dvd_rfl ?_
-  conv_lhs => rw [← tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le, pow_succ']
+  conv_lhs => rw [← tsub_add_cancel_of_le (Nat.Prime.one_lt hpri.out).le, pow_succ]
   exact mul_dvd_mul_right (associated_zeta_sub_one_pow_prime hζ).dvd _
 
 namespace KummersLemma
@@ -86,7 +86,7 @@ lemma map_poly : (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) =
     RingHom.coe_coe, Subalgebra.coe_val, one_div, map_sub, map_one, coeff_add, coeff_sub,
     PNat.pos, pow_eq_zero_iff, this, mul_add, IsPrimitiveRoot.val_unit'_coe]
   simp_rw [← smul_eq_mul K, ← coeff_smul]
-  rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left, smul_sub, smul_C,
+  rw [smul_C, smul_eq_mul, ← smul_pow, ← mul_div_assoc, mul_div_cancel_left₀, smul_sub, smul_C,
     smul_eq_mul, mul_inv_cancel, map_one, Algebra.smul_def, ← C_eq_algebraMap, map_sub, map_one]
   exact hζ.sub_one_ne_zero hpri.out.one_lt
   exact pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt)
@@ -95,13 +95,13 @@ lemma irreducible_map_poly :
     Irreducible ((poly hp hζ u hcong).map (algebraMap (𝓞 K) K)) := by
   rw [map_poly, ← irreducible_taylor_iff (r := 1 / (ζ - 1))]
   simp only [taylor, one_div, map_add, LinearMap.coe_mk, AddHom.coe_mk, pow_comp, sub_comp,
-    X_comp, C_comp, add_sub_cancel]
+    X_comp, C_comp, add_sub_cancel_right]
   rw [← sub_neg_eq_add, ← (C : K →+* _).map_neg]
   apply X_pow_sub_C_irreducible_of_prime hpri.out
   intro b hb
   apply hu (- b * (ζ - 1))
   rw [mul_pow, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow, hb, neg_neg,
-    div_mul_cancel _ (pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt))]
+    div_mul_cancel₀ _ (pow_ne_zero _ (hζ.sub_one_ne_zero hpri.out.one_lt))]
 
 theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
     (e : α ^ (p : ℕ) = algebraMap K L u) (m : ℕ) :
@@ -113,7 +113,7 @@ theorem aeval_poly {L : Type*} [Field L] [Algebra K L] (α : L)
     (poly_spec hp hζ u hcong)
   simp only [map_sub, map_one, map_pow, map_mul, aeval_C, Subalgebra.algebraMap_eq, smul_pow,
     RingHom.coe_comp, RingHom.coe_coe, Subalgebra.coe_val, Function.comp_apply, e,
-    IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left _ hζ',
+    IsPrimitiveRoot.val_unit'_coe, map_add, aeval_X, ← mul_div_assoc, mul_div_cancel_left₀ _ hζ',
     sub_sub_cancel_left, (hpri.out.odd_of_ne_two (PNat.coe_injective.ne hp)).neg_pow] at this
   rw [← pow_mul, mul_comm m, pow_mul, hζ.pow_eq_one, one_pow, one_smul, add_left_neg,
     mul_eq_zero] at this
@@ -142,14 +142,14 @@ theorem roots_poly {L : Type*} [Field L] [Algebra K L] (α : L)
       simp only [Finset.image_val, Finset.range_val, Multiset.mem_dedup, Multiset.mem_map,
         Multiset.mem_range] at hx
       obtain ⟨m, _, rfl⟩ := hx
-      rw [mem_roots, IsRoot.def, eval_map, ← aeval_def, aeval_poly hp hζ u hcong α e]
+      rw [mem_roots, IsRoot.definition, eval_map, ← aeval_def, aeval_poly hp hζ u hcong α e]
       exact ((monic_poly hp hζ u hcong).map (algebraMap (𝓞 K) L)).ne_zero
     · intros i hi j hj e
       apply (hζ.map_of_injective (algebraMap K L).injective).injOn_pow_mul hα hi hj
       apply_fun (1 - · * (algebraMap K L ζ - 1)) at e
       dsimp only at e
       simpa only [Nat.cast_one, map_sub, map_one, Algebra.smul_def, map_pow,
-        div_mul_cancel _ hζ', sub_sub_cancel] using e
+        div_mul_cancel₀ _ hζ', sub_sub_cancel] using e
   · simp only [Finset.range_val, Multiset.card_map, Multiset.card_range]
     refine (Polynomial.card_roots' _).trans ?_
     rw [(monic_poly hp hζ u hcong).natDegree_map, natDegree_poly hp hζ]
@@ -253,7 +253,7 @@ lemma separable_poly_aux {L : Type*} [Field L] [Algebra K L] (α : L)
     sub_sub_sub_cancel_left, Submonoid.coe_mul, Subsemiring.coe_toSubmonoid,
     Subalgebra.coe_toSubsemiring]
   rw [← sub_div, ← sub_smul, ← hv, Algebra.smul_def, map_mul, map_sub, map_one, mul_assoc,
-    mul_div_cancel_left _ hζ']
+    mul_div_cancel_left₀ _ hζ']
   rfl
 
 open scoped KummerExtension in
@@ -283,7 +283,7 @@ lemma polyRoot_spec {L : Type*} [Field L] [Algebra K L] (α : L)
     α = (ζ ^ i)⁻¹ • (1 - (ζ - 1) • (polyRoot hp hζ u hcong α e i : L)) := by
   apply smul_right_injective (M := L) (c := ζ ^ i) (pow_ne_zero _ <| hζ.ne_zero p.pos.ne.symm)
   simp only [polyRoot, map_sub, map_one, Algebra.smul_def (ζ - 1), ← mul_div_assoc,
-    mul_div_cancel_left _
+    mul_div_cancel_left₀ _
       ((hζ.map_of_injective (algebraMap K L).injective).sub_one_ne_zero hpri.out.one_lt),
     sub_sub_cancel, smul_smul, inv_mul_cancel (pow_ne_zero _ <| hζ.ne_zero p.pos.ne.symm), one_smul]
 
diff --git a/FltRegular/NumberTheory/QuotientTrace.lean b/FltRegular/NumberTheory/QuotientTrace.lean
index 5970d7cb..1b79ddba 100644
--- a/FltRegular/NumberTheory/QuotientTrace.lean
+++ b/FltRegular/NumberTheory/QuotientTrace.lean
@@ -185,7 +185,7 @@ lemma comap_map_eq_map_of_isLocalization_algebraMapSubmonoid :
     · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
         map_mul, hβ, inv_mul_cancel, sub_self]
       rwa [Ne.def, Ideal.Quotient.eq_zero_iff_mem]
-    · rw [add_sub_cancel'_right]
+    · rw [add_sub_cancel]
   have := Ideal.mul_mem_left _ (algebraMap _ _ β) hαx
   rw [← Algebra.smul_def, smul_smul, hβ, add_smul, one_smul] at this
   refine (Submodule.add_mem_iff_left _ ?_).mp this
@@ -216,7 +216,7 @@ def quotMapEquivQuotMapMaximalIdealOfIsLocalization : S ⧸ pS ≃+* Sₚ ⧸ pS
       · rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one,
           map_mul, hβ, mul_inv_cancel, sub_self]
         rwa [Ne.def, Ideal.Quotient.eq_zero_iff_mem]
-      · rw [add_sub_cancel'_right]
+      · rw [add_sub_cancel]
     use β • x
     rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq,
       RingHom.comp_apply, ← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
@@ -229,7 +229,7 @@ def quotMapEquivQuotMapMaximalIdealOfIsLocalization : S ⧸ pS ≃+* Sₚ ⧸ pS
     simp only
     rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul,
       IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ← Algebra.smul_def, smul_smul,
-      hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel]
+      hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]
 
 lemma trace_quotient_eq_trace_localization_quotient (x) :
     Algebra.trace (R ⧸ p) (S ⧸ pS) (Ideal.Quotient.mk pS x) =
diff --git a/FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean
index b0a57248..8bae9784 100644
--- a/FltRegular/ReadyForMathlib/PowerBasis.lean
+++ b/FltRegular/ReadyForMathlib/PowerBasis.lean
@@ -35,10 +35,10 @@ theorem exists_int_sModEq (x : 𝓞 K) :
       congr
       rfl
       ext i
-      rw [this i, _root_.pow_succ, ← mul_assoc, mul_comm _ pb.gen, mul_assoc]
+      rw [this i, _root_.pow_succ, ← mul_assoc, mul_comm _ pb.gen]
     rw [← mul_sum] at H
     nth_rw 1 [← H]
-    rw [SModEq.sub_mem, mul_one, add_sub_cancel', mul_comm, mem_span_singleton']
+    rw [SModEq.sub_mem, mul_one, add_sub_cancel_left, mul_comm, mem_span_singleton']
     exact ⟨_, rfl⟩
   · exact not_mem_erase (⟨0, pb.dim_pos⟩ : Fin pb.dim) univ
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 0a1d03ef..e4aba471 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "f3447c3732c9d6e8df3bdad78e5ecf7e8b353bbc",
+   "rev": "67c40f89be2c17c6f4b0b6056d2de8591c0f92d3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "bbcffbcc19d69e13d5eea716283c76169db524ba",
+   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "7f61923ac7a0b566f4d0ab98bb87446bbfe416ec",
+   "rev": "1cca755bf20cfcec06dc01cdf4efac4e80b635eb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -76,7 +76,7 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "5b096942260d7805cc90bacf4ea4a0f8e9700ccb",
+   "rev": "6a350f4ec7323a4e8ad6bf50736f779853d441e9",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -94,7 +94,7 @@
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "780bbec107cba79d18ec55ac2be3907a77f27f98",
+   "rev": "a34d3c1f7b72654c08abe5741d94794db40dbb2e",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",