bump

FltRegular/CaseI/AuxLemmas.lean

@@ -60,7 +60,7 @@ theorem aux0k₁ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   symm
   intro habs
   rw [show (k₁ : ℤ) = 0 by simpa using habs, zero_sub] at hcong
-  rw [habs, _root_.pow_zero, mul_one, add_sub_cancel', aux_cong0k₁ hpri hcong] at hdiv
+  rw [habs, _root_.pow_zero, mul_one, add_sub_cancel_left, aux_cong0k₁ hpri hcong] at hdiv
   nth_rw 1 [show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
   have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₁ b p j • ζ ^ j := by
     convert hdiv using 1
@@ -192,7 +192,6 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   rw [habs, pow_one, aux_cong1k₂ hpri hp5 hcong] at hdiv
   ring_nf at hdiv
   have key : ↑(p : ℤ) ∣ ∑ j in range p, f1k₂ a j • ζ ^ j := by
-    rw [Int.cast_ofNat]
     suffices ∑ j in range p, f1k₂ a j • ζ ^ j = ↑a - ↑a * ζ ^ 2 by
       rwa [this]
     simp_rw [f1k₂, ite_smul, sum_ite, filter_filter, ← Ne.def, ne_and_eq_iff_right

FltRegular/CaseI/Statement.lean

@@ -92,33 +92,6 @@ theorem ab_coprime {a b c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0)
   rw [hgcd] at Hq
   exact hqpri.not_unit (isUnit_of_dvd_one Hq)
 
-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 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⟩ ℚ)) _ (foo2 p)
-
-noncomputable
-instance foo4 : @NormalizedGCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)))
-  (@IsDomain.toCancelCommMonoidWithZero _ (@IdemCommSemiring.toCommSemiring _
-    Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule) (foo3 p)) := by
-  convert @Ideal.instNormalizedGCDMonoidIdealToSemiringToCommSemiringCancelCommMonoidWithZero _ _ (foo2 p)
-
-noncomputable
-instance foo5 : @GCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ)))
-  (@IsDomain.toCancelCommMonoidWithZero _ (@IdemCommSemiring.toCommSemiring _
-    Submodule.instIdemCommSemiringSubmoduleToSemiringToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringToModule) (foo3 p)) := by
-  convert @NormalizedGCDMonoid.toGCDMonoid (Ideal (𝓞 (CyclotomicField ⟨p, hpri.out.pos⟩ ℚ))) _ (foo4 p)
-
-variable {p}
-
 theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
     (hgcd : ({ a, b, c } : Finset ℤ).gcd id = 1)
     (caseI : ¬↑p ∣ a * b * c) {ζ : R} (hζ : ζ ∈ nthRootsFinset p R) :
@@ -192,7 +165,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     rw [natAbs_ofNat]
     exact emod_lt_of_pos _ (by simp [hpri.out.pos])
   · simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.int_cast_eq_int_cast_iff,
-      ZMod.int_cast_mod, Int.cast_sub, Int.cast_mul, int_cast_ofNat, Int.cast_one]
+      ZMod.int_cast_mod, Int.cast_sub, Int.cast_mul, Int.cast_natCast, Int.cast_one]
   simp only [add_sub_assoc, sub_sub] at hk ⊢
   convert hk using 3
   rw [mul_add, mul_comm (↑a : R), ← mul_assoc _ (↑b : R), mul_comm _ (↑b : R), mul_assoc (↑b : R)]
@@ -203,15 +176,15 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     refine' eq_of_div_eq_one _
     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]
+      Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, Int.cast_natCast, 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_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]
+      Int.cast_sub, ZMod.int_cast_mod, Int.cast_mul, Int.cast_natCast, Int.cast_one, sub_self]
 
 /-- Auxiliary function -/
 def f (a b : ℤ) (k₁ k₂ : ℕ) : ℕ → ℤ := fun x =>

FltRegular/FltThree/Edwards.lean

@@ -28,7 +28,7 @@ theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm.na
 
 theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ abs z.re = 1 ∧ z.im = 0 :=
   by
-  rw [← Zsqrtd.norm_eq_one_iff, ← Int.coe_nat_inj', Int.ofNat_one,
+  rw [← Zsqrtd.norm_eq_one_iff, ← Int.natCast_inj, Int.ofNat_one,
     Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)]
   refine' ⟨Spts.eq_one, fun h => _⟩
   rw [Zsqrtd.norm_def, h.2, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, h.1, one_pow]
@@ -39,7 +39,7 @@ theorem Zsqrt3.coe_of_isUnit {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : Units ℤ
   obtain ⟨v, hv⟩ : IsUnit z.re := by rwa [Int.isUnit_iff_abs_eq]
   use v
   rw [Zsqrtd.ext_iff, hu, ← hv]
-  simp only [Zsqrtd.coe_int_re, and_true_iff, eq_self_iff_true, Zsqrtd.coe_int_im]
+  simp only [Zsqrtd.intCast_re, and_true_iff, eq_self_iff_true, Zsqrtd.intCast_im]
 
 theorem Zsqrt3.coe_of_isUnit' {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : ℤ, z = u ∧ abs u = 1 :=
   by
@@ -337,8 +337,8 @@ theorem no_conj (s : Multiset (ℤ√(-3))) {p : ℤ√(-3)} (hp : ¬IsUnit p)
     rw [Multiset.prod_cons, Multiset.prod_cons, ← mul_assoc, ← Zsqrtd.norm_eq_mul_conj] at hcoprime
     rw [Zsqrtd.isUnit_iff_norm_isUnit]
     apply IsCoprime.isUnit_of_dvd' hcoprime <;>
-      simp only [add_zero, Zsqrtd.coe_int_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re,
-        MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.coe_int_im]
+      simp only [add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re,
+        MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.intCast_im]
 
 /-- Associated elements in `ℤ√-3`. -/
 def Associated' (x y : ℤ√(-3)) : Prop :=
@@ -438,7 +438,7 @@ theorem eq_or_eq_conj_of_associated_of_re_zero {x A : ℤ√(-3)} (hx : x.re = 0
   obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit
   have hA : A.re = 0 := by
     simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero,
-      Zsqrtd.coe_int_im]
+      Zsqrtd.intCast_im]
   rw [abs_eq <| zero_le_one' ℤ] at hv2
   cases' hv2 with hv2 hv2
   · left

FltRegular/FltThree/FltThree.lean

@@ -30,7 +30,7 @@ theorem exists_coprime {n : ℕ} (hn : 0 < n) {a b c : ℤ} (ha' : a ≠ 0) (hb'
     rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
     exact dvd_mul_right _ _
   have hdpos : 0 < d := Int.gcd_pos_of_ne_zero_left _ ha'
-  have hd := Int.coe_nat_ne_zero_iff_pos.mpr hdpos
+  have hd := Int.natCast_ne_zero_iff_pos.mpr hdpos
   have hsoln : A ^ n + B ^ n = C ^ n :=
     by
     apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd)
@@ -227,7 +227,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
       have H := dvd_mul_right 2 p
       rw [hP] at H
       apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left
-      rw [Int.coe_nat_dvd_right]
+      rw [Int.dvd_natCast]
       change ¬2 ∣ d
       rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime]
       exact hne2.symm
@@ -237,14 +237,14 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
       exact dvd_mul_right _ _
     · have h000 : d ∣ 3 * q.natAbs ^ 2 :=
         by
-        rw [← Int.coe_nat_dvd, Int.ofNat_mul, Int.coe_nat_pow, Int.natAbs_sq, Nat.cast_three]
+        rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.coe_nat_pow, Int.natAbs_sq, Nat.cast_three]
         use Q - d * H ^ 2
         rw [mul_sub, ← hQ, hp]
         ring
       cases' (Nat.Prime.dvd_mul hdprime).mp h000 with h000 h000
       · rw [Nat.prime_dvd_prime_iff_eq hdprime Nat.prime_three] at h000
         exact absurd h000 hne3
-      · rw [Int.coe_nat_dvd_left]
+      · rw [Int.natCast_dvd]
         exact Nat.Prime.dvd_of_dvd_pow hdprime h000
   set k := g.factors.length
   have hg : g = 3 ^ k := by
@@ -255,7 +255,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
       apply mul_pos zero_lt_two
       rwa [pos_iff_ne_zero, Int.natAbs_ne_zero]
     intro d hdprime hddvdg
-    rw [← Int.coe_nat_dvd] at hddvdg
+    rw [← Int.natCast_dvd_natCast] at hddvdg
     apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg']
     exacts[Int.gcd_dvd_left, Int.gcd_dvd_right]
   refine' ⟨k, hg, _⟩

FltRegular/FltThree/Spts.lean

@@ -95,8 +95,8 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime
       rw [Zsqrtd.norm_def, HAsq]
       ring
     rw [mul_comm _ U, ← mul_assoc, ← HU, HX]
-    simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.coe_int_re, MulZeroClass.zero_mul, mul_neg,
-      Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.coe_int_im,
+    simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, mul_neg,
+      Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.intCast_im,
       this]
     constructor <;> ring
 
@@ -144,7 +144,7 @@ theorem factors' (a : ℤ√(-3)) (f : ℤ) (g : ℤ) (hodd : Odd f) (hgpos : g
     · apply_fun abs  at hfactor
       rw [abs_mul, h, mul_one, abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] at hfactor
       exact ⟨_, hfactor⟩
-    · rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.coe_nat_inj'] at h
+    · rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.natCast_inj] at h
       obtain ⟨p, pprime, pdvd⟩ := Int.exists_prime_and_dvd h
       have : p ∣ a.norm := by
         rw [← hfactor]
@@ -190,9 +190,9 @@ theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) :
   set c' : ℤ√(-3) := ⟨c, d⟩
   refine' ⟨c', ⟨m, n⟩, _, _⟩
   ·
-    simp only [Zsqrtd.ext_iff, ha, hb, add_zero, Zsqrtd.coe_int_re, eq_self_iff_true, Zsqrtd.mul_im,
+    simp only [Zsqrtd.ext_iff, ha, hb, add_zero, Zsqrtd.intCast_re, eq_self_iff_true, Zsqrtd.mul_im,
       zero_add, Zsqrtd.add_im, and_self_iff, Zsqrtd.mul_re, MulZeroClass.mul_zero, Zsqrtd.add_re,
-      Zsqrtd.coe_int_im]
+      Zsqrtd.intCast_im]
   · rw [← mul_lt_mul_left (by norm_num : (0 : ℤ) < 4)]
     calc
       4 * c'.norm = (2 * c) ^ 2 + 3 * (2 * d) ^ 2 :=
@@ -227,16 +227,16 @@ theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x|
       set e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im with he
       convert dvd_sub hfactor (dvd_mul_right x e)
       rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def]
-      simp only [Zsqrtd.coe_int_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
-        Zsqrtd.coe_int_im]
+      simp only [Zsqrtd.intCast_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
+        Zsqrtd.intCast_im]
       ring
     refine' ⟨y, hy, _⟩
     have h0'' : 0 < x.natAbs := by
       zify
       exact zero_lt_one.trans h
     rw [← mul_lt_mul_left h0'', ← pow_two, ← Int.natAbs_mul, ← hy]
     zify
-    rwa [← Int.coe_natAbs x, Int.natAbs_pow_two x, ← Int.coe_natAbs,
+    rwa [← Int.natCast_natAbs x, Int.natAbs_pow_two x, ← Int.natCast_natAbs,
       Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) c)]
 
 -- Edwards p50 step (5')
@@ -285,11 +285,9 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
             ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
           (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _)
     have := Zsqrtd.coprime_of_dvd_coprime hcoprime this
-    simp only [Zsqrtd.coe_int_re, isCoprime_zero_right, Zsqrtd.coe_int_im, hpprime.not_unit] at this
-  have h6 : x * z = C'.norm :=
-    by
-    have hgnezero := Int.coe_nat_ne_zero_iff_pos.mpr hgpos
-    apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 hgnezero)
+    simp only [Zsqrtd.intCast_re, isCoprime_zero_right, Zsqrtd.intCast_im, hpprime.not_unit] at this
+  have h6 : x * z = C'.norm := by
+    apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 <| Int.natCast_ne_zero_iff_pos.mpr hgpos)
     rw [← h5, hz, mul_left_comm]
   have h8 : z ≠ 0 := by
     apply right_ne_zero_of_mul

FltRegular/MayAssume/Lemmas.lean

@@ -61,7 +61,7 @@ theorem p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp : p
     mul_eq_zero] at h
   rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
   refine' Or.resolve_right h fun h3 => _
-  rw [show ↑(3 : ℤ) = ((3 : ℕ) : ZMod p) by simp, ZMod.nat_cast_zmod_eq_zero_iff_dvd,
+  rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.nat_cast_zmod_eq_zero_iff_dvd,
     Nat.dvd_prime Nat.prime_three] at h3
   cases' h3 with H₁ H₂
   · exact hpri.ne_one H₁

FltRegular/NumberTheory/AuxLemmas.lean

@@ -1,6 +1,6 @@
 import Mathlib.NumberTheory.RamificationInertia
 import Mathlib.RingTheory.Trace
-import Mathlib.Data.Polynomial.Taylor
+import Mathlib.Algebra.Polynomial.Taylor
 import Mathlib.RingTheory.Valuation.ValuationRing
 
 /-!

FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean

@@ -203,9 +203,9 @@ lemma zeta_sub_one_pow_dvd_norm_sub_pow (x : 𝓞 K) :
   obtain ⟨s, hs⟩ := zeta_sub_one_dvd_trace_sub_smul hζ x
   obtain ⟨t, ht⟩ := (associated_zeta_sub_one_pow_prime hζ).dvd
   rw [sub_eq_iff_eq_add] at hs
-  simp only [zsmul_eq_mul, Int.cast_ofNat] at hr
+  simp only [zsmul_eq_mul, Int.cast_natCast] at hr
   simp only [nsmul_eq_mul, hr, Int.cast_add, Int.cast_one, Int.cast_mul, hs, ge_iff_le, PNat.pos,
-    Nat.cast_pred, Int.cast_ofNat, Int.cast_pow, Nat.cast_mul, ne_eq, PNat.ne_zero,
+    Nat.cast_pred, Int.cast_pow, Nat.cast_mul, ne_eq, PNat.ne_zero, Int.cast_natCast,
     not_false_eq_true, isUnit_pow_iff]
   suffices (hζ.unit' - 1 : 𝓞 K) ^ (p : ℕ) ∣ (hζ.unit' - 1) * p * s + (p : 𝓞 K) ^ 2 * (r + x) by
     convert this using 1; ring
@@ -231,9 +231,9 @@ lemma norm_add_one_smul_of_isUnit {K} [Field K] [NumberField K] {p : ℕ} (hpri
     intro e; apply hp
     obtain ⟨r, hr⟩ := Algebra.norm_one_add_smul (p : ℤ) x
     have : (p : ℤ) * (- Algebra.trace ℤ _ x - r * p) = 2 := by
-      rw [zsmul_eq_mul, Int.cast_ofNat, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
+      rw [zsmul_eq_mul, Int.cast_natCast, ← nsmul_eq_mul, e, eq_comm, ← sub_eq_zero] at hr
       rw [eq_comm, ← sub_eq_zero, ← hr]
       ring
     exact (Nat.prime_two.eq_one_or_self_of_dvd _
-      (Int.coe_nat_dvd.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one
+      (Int.natCast_dvd_natCast.mp ⟨_, this.symm⟩)).resolve_left hpri.ne_one
   exact H.resolve_right this