bump

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]

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]

FltRegular/CaseII/InductionStep.lean

@@ -60,15 +60,15 @@ 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 η⟩
 
 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]

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]

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

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

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

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

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

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

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