fix build

Author: riccardobrasca

FltRegular/CaseI/AuxLemmas.lean

@@ -30,7 +30,7 @@ theorem aux_cong0k₁ {k : Fin p} (hcong : k ≡ -1 [ZMOD p]) :
   refine' Fin.ext _
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = p.pred by simpa
-  rw [← ZMod.int_cast_eq_int_cast_iff] at hcong
+  rw [← ZMod.intCast_eq_intCast_iff] at hcong
   rw [hcong, cast_neg, Int.cast_one, pred_eq_sub_one]
   haveI : NeZero p := ⟨hpri.ne_zero⟩
   haveI : Fact p.Prime := ⟨hpri⟩
@@ -84,7 +84,7 @@ theorem aux_cong0k₂ {k : Fin p} (hcong : k ≡ 1 [ZMOD p]) : k = ⟨1, hpri.on
   refine' Fin.ext _
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 1 by simpa
-  rw [← ZMod.int_cast_eq_int_cast_iff] at hcong
+  rw [← ZMod.intCast_eq_intCast_iff] at hcong
   rw [hcong, Int.cast_one]
   haveI : Fact p.Prime := ⟨hpri⟩
   simp [ZMod.val_one]
@@ -106,8 +106,8 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ
   symm
   intro habs
   replace hcong := hcong.symm
-  rw [show (k₂ : ℤ) = 0 by simpa using habs, ← ZMod.int_cast_eq_int_cast_iff, Int.cast_sub,
-    Int.cast_zero, sub_eq_zero, ZMod.int_cast_eq_int_cast_iff] at hcong
+  rw [show (k₂ : ℤ) = 0 by simpa using habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub,
+    Int.cast_zero, sub_eq_zero, ZMod.intCast_eq_intCast_iff] at hcong
   rw [habs, _root_.pow_zero, mul_one, aux_cong0k₂ hpri hcong, Fin.val_mk, pow_one, add_sub_assoc,
     ← sub_mul, add_sub_right_comm, show ζ = ζ ^ ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) by simp] at hdiv
   have key : ↑(p : ℤ) ∣ ∑ j in range p, f0k₂ a b j • ζ ^ j := by
@@ -119,7 +119,7 @@ theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ
   rw [sum_range] at key
   refine' hab _
   symm
-  rw [← ZMod.int_cast_eq_int_cast_iff, ZMod.int_cast_eq_int_cast_iff_dvd_sub]
+  rw [← ZMod.intCast_eq_intCast_iff, ZMod.intCast_eq_intCast_iff_dvd_sub]
   have hpri₁ : (P : ℕ).Prime := hpri
   simpa [f0k₂] using dvd_coeff_cycl_integer hpri₁ hζ (auxf0k₂ hpri hp5 a b) key ⟨0, hpri.pos⟩
 
@@ -131,7 +131,7 @@ theorem aux_cong1k₁ {k : Fin p} (hcong : k ≡ 0 [ZMOD p]) : k = ⟨0, hpri.po
   refine' Fin.ext _
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 0 by simpa
-  rw [← ZMod.int_cast_eq_int_cast_iff] at hcong
+  rw [← ZMod.intCast_eq_intCast_iff] at hcong
   rw [hcong, Int.cast_zero]
   haveI : Fact p.Prime := ⟨hpri⟩
   simp
@@ -158,7 +158,7 @@ theorem aux_cong1k₂ {k : Fin p} (hpri : p.Prime) (hp5 : 5 ≤ p) (hcong : k 
   refine' Fin.ext _
   rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
   suffices ((k : ℤ) : ZMod p).val = 2 by simpa
-  rw [← ZMod.int_cast_eq_int_cast_iff] at hcong
+  rw [← ZMod.intCast_eq_intCast_iff] at hcong
   rw [hcong]
   simp only [Int.cast_add, algebraMap.coe_one]
   haveI : Fact p.Prime := ⟨hpri⟩
@@ -187,8 +187,8 @@ theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot 
   symm
   intro habs
   replace hcong := hcong.symm
-  rw [show (k₂ : ℤ) = 1 by simpa using habs, ← ZMod.int_cast_eq_int_cast_iff, Int.cast_sub,
-    sub_eq_iff_eq_add, ← Int.cast_add, ZMod.int_cast_eq_int_cast_iff] at hcong
+  rw [show (k₂ : ℤ) = 1 by simpa using habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub,
+    sub_eq_iff_eq_add, ← Int.cast_add, ZMod.intCast_eq_intCast_iff] at hcong
   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
@@ -212,7 +212,7 @@ theorem auxk₁k₂ {k₁ k₂ : Fin p} (hpri : p.Prime) (hcong : k₂ ≡ k₁
     (k₁ : ℕ) ≠ (k₂ : ℕ) := by
   haveI := (⟨hpri⟩ : Fact p.Prime)
   intro habs
-  rw [habs, ← ZMod.int_cast_eq_int_cast_iff, Int.cast_sub, ← sub_eq_zero] at hcong
+  rw [habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub, ← sub_eq_zero] at hcong
   simp at hcong
 
 end KoneKtwo

FltRegular/CaseI/Statement.lean

@@ -164,8 +164,8 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     refine' natAbs_lt_natAbs_of_nonneg_of_lt (emod_nonneg _ hpcoe) _
     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_natCast, Int.cast_one]
+  · simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_eq_intCast_iff,
+      ZMod.intCast_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)]
@@ -175,16 +175,16 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
       IsPrimitiveRoot.coe_unit'_coe]
     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_natCast, sub_self]
+    simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
+      Int.cast_sub, ZMod.intCast_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_natCast, Int.cast_one, sub_self]
+    simp only [natAbs_of_nonneg (emod_nonneg _ hpcoe), ← ZMod.intCast_zmod_eq_zero_iff_dvd,
+      Int.cast_sub, ZMod.intCast_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

@@ -145,7 +145,7 @@ theorem step1'' {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hp : p.norm
           simp [Zsqrtd.ext_iff, hp', h5]
       simp only [hp', one_mul, Zsqrtd.norm_neg, Int.cast_one, Int.cast_neg, neg_one_mul]
       cases h4 <;> cases h2 <;> simp [*]
-  · rw [Zsqrtd.norm_mul, Zsqrtd.norm_int_cast, ← sq, ← sq_abs, hp', one_pow, one_mul]
+  · rw [Zsqrtd.norm_mul, Zsqrtd.norm_intCast, ← sq, ← sq_abs, hp', one_pow, one_mul]
     cases' h2 with h2 h2 <;>
       · rw [h2, Zsqrtd.norm_mul]
         congr

FltRegular/FltThree/FltThree.lean

@@ -27,7 +27,7 @@ theorem exists_coprime {n : ℕ} (hn : 0 < n) {a b c : ℤ} (ha' : a ≠ 0) (hb'
   obtain ⟨B, HB⟩ : ↑d ∣ b := @Int.gcd_dvd_right a b
   obtain ⟨C, HC⟩ : ↑d ∣ c :=
     by
-    rw [← Int.pow_dvd_pow_iff hn, ← h, HA, HB, mul_pow, mul_pow, ← mul_add]
+    rw [← Int.pow_dvd_pow_iff hn.ne', ← 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.natCast_ne_zero_iff_pos.mpr hdpos
@@ -89,7 +89,7 @@ theorem flt_not_add_self {a b c : ℤ} (ha : a ≠ 0) (h : a ^ 3 + b ^ 3 = c ^ 3
   rw [← mul_two] at h
   obtain ⟨d, rfl⟩ : a ∣ c :=
     by
-    rw [← Int.pow_dvd_pow_iff (by norm_num : 0 < 3), ← h]
+    rw [← Int.pow_dvd_pow_iff (by norm_num : 3 ≠ 0), ← h]
     apply dvd_mul_right
   apply Int.two_not_cube d
   rwa [mul_pow, mul_right_inj' (pow_ne_zero 3 ha), eq_comm] at h
@@ -276,7 +276,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
       apply dvd_mul_right
     exact dvd_trans this Int.gcd_dvd_left
   apply IsCoprime.isUnit_of_dvd' hcoprime hdvdp
-  · rw [← Int.pow_dvd_pow_iff zero_lt_two] at hdvdp
+  · rw [← Int.pow_dvd_pow_iff two_ne_zero] at hdvdp
     apply Prime.dvd_of_dvd_pow Int.prime_three
     rw [← mul_dvd_mul_iff_left (three_ne_zero' ℤ), ← pow_two, ← dvd_add_right hdvdp]
     refine' dvd_trans _ Int.gcd_dvd_right
@@ -610,7 +610,7 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime :
   obtain ⟨e, he⟩ := hcubeleft
   have : 3 ∣ e :=
     by
-    rw [← Int.pow_dvd_pow_iff (by norm_num : 0 < 3), ← he, hs]
+    rw [← Int.pow_dvd_pow_iff (by norm_num : 3 ≠ 0), ← he, hs]
     convert dvd_mul_right _ (2 * v * (u - v) * (u + v)) using 1
     norm_num
     ring

FltRegular/FltThree/Spts.lean

@@ -266,7 +266,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
   have hgpos : 0 < g := by rwa [hg, Zsqrtd.gcd_pos_iff]
   obtain ⟨C', HC', HCDcoprime⟩ := Zsqrtd.exists_coprime_of_gcd_pos hgpos
   have h5 : x * y = (g : ℤ) ^ 2 * C'.norm := by
-    rw [← hy, HC', Zsqrtd.norm_mul, Zsqrtd.norm_int_cast, ← pow_two]
+    rw [← hy, HC', Zsqrtd.norm_mul, Zsqrtd.norm_intCast, ← pow_two]
   obtain ⟨z, hz⟩ : (g : ℤ) ^ 2 ∣ y :=
     by
     have : (g : ℤ) ^ 2 ∣ x * y := by

FltRegular/MayAssume/Lemmas.lean

@@ -53,15 +53,15 @@ theorem p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp : p
   letI : Fact p.Prime := ⟨hpri⟩
   replace h := congr_arg (fun n : ℤ => (n : ZMod p)) h
   simp only [Int.coe_nat_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h
-  simp only [← ZMod.int_cast_eq_int_cast_iff, Int.cast_neg] at hbc hab
+  simp only [← ZMod.intCast_eq_intCast_iff, Int.cast_neg] at hbc hab
   rw [hab, hbc, ← sub_eq_zero, ← sub_eq_add_neg, ← Int.cast_neg, ← Int.cast_sub,
     ← Int.cast_sub] at h
   ring_nf at h
   simp only [Int.cast_neg, Int.cast_mul, Int.cast_one, Int.cast_ofNat, neg_eq_zero,
     mul_eq_zero] at h
-  rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd]
+  rw [← ZMod.intCast_zmod_eq_zero_iff_dvd]
   refine' Or.resolve_right h fun h3 => _
-  rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.nat_cast_zmod_eq_zero_iff_dvd,
+  rw [show (3 : ZMod p) = ((3 : ℕ) : ZMod p) by simp, ZMod.natCast_zmod_eq_zero_iff_dvd,
     Nat.dvd_prime Nat.prime_three] at h3
   cases' h3 with H₁ H₂
   · exact hpri.ne_one H₁
@@ -100,9 +100,9 @@ theorem a_not_cong_b {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp5 : 5 ≤ p) (h
     · simp [H₂, H₃]
     · simp [H₂, H₄]
   · have hp3 : p ≠ 3 := by linarith
-    rw [← ZMod.int_cast_eq_int_cast_iff] at habs H
+    rw [← ZMod.intCast_eq_intCast_iff] at habs H
     rw [H] at habs
-    rw [ZMod.int_cast_eq_int_cast_iff] at habs H
+    rw [ZMod.intCast_eq_intCast_iff] at habs H
     obtain ⟨n, hn⟩ := p_dvd_c_of_ab_of_anegc hpri hp3 h H habs
     refine' caseI ⟨a * b * n, _⟩
     rw [hn]

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -310,10 +310,10 @@ theorem aux_lem_flt [Fact (p : ℕ).Prime] {x y z : ℤ} (H : x ^ (p : ℕ) + y
     (caseI : ¬↑p ∣ x * y * z) : ¬(p : ℤ) ∣ (x + y : ℤ) := by
   intro habs
   replace habs : ↑(p : ℕ) ∣ (x + y : ℤ) := by simpa using habs
-  rw [← ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.cast_add] at habs
+  rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, Int.cast_add] at habs
   replace H := congr_arg (fun x : ℤ => (x : ZMod p)) H.symm
   simp only [Int.cast_add, Int.cast_pow, ZMod.pow_card, habs,
-    ZMod.int_cast_zmod_eq_zero_iff_dvd] at H
+    ZMod.intCast_zmod_eq_zero_iff_dvd] at H
   exact caseI (Dvd.dvd.mul_left H _)
 
 theorem fltIdeals_coprime (hpri : (p : ℕ).Prime) (p5 : 5 ≤ p) {x y z : ℤ}