bump

Author: Ruben-VandeVelde

FltRegular/FltThree/FltThree.lean

@@ -237,7 +237,7 @@ 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.natCast_dvd_natCast, Int.ofNat_mul, Int.coe_nat_pow, Int.natAbs_sq, Nat.cast_three]
+        rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three]
         use Q - d * H ^ 2
         rw [mul_sub, ← hQ, hp]
         ring

FltRegular/FltThree/Spts.lean

@@ -67,7 +67,7 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime
   · set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX
     obtain ⟨U, HU⟩ : (p.norm : ℤ√(-3)) ∣ X :=
       by
-      rw [Zsqrtd.coe_int_dvd_iff]
+      rw [Zsqrtd.intCast_dvd]
       refine' ⟨_, HA⟩
       apply @Prime.dvd_of_dvd_pow _ _ _ hpprime _ 2
       have : X.re ^ 2 = X.norm - 3 * X.im ^ 2 :=
@@ -282,8 +282,8 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod
       exact
         dvd_add
           (dvd_mul_of_dvd_left
-            ((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) _)
+            ((Zsqrtd.intCast_dvd_intCast _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
+          (dvd_mul_of_dvd_right ((Zsqrtd.intCast_dvd_intCast _ _).mpr hpdvdright) _)
     have := Zsqrtd.coprime_of_dvd_coprime hcoprime this
     simp only [Zsqrtd.intCast_re, isCoprime_zero_right, Zsqrtd.intCast_im, hpprime.not_unit] at this
   have h6 : x * z = C'.norm := by

FltRegular/MayAssume/Lemmas.lean

@@ -51,7 +51,7 @@ theorem p_dvd_c_of_ab_of_anegc {p : ℕ} {a b c : ℤ} (hpri : p.Prime) (hp : p
     (h : a ^ p + b ^ p = c ^ p) (hab : a ≡ b [ZMOD p]) (hbc : b ≡ -c [ZMOD p]) : ↑p ∣ c := by
   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 [Int.natCast_pow, Int.cast_add, Int.cast_pow, ZMod.pow_card] at h
   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

FltRegular/NumberTheory/Cyclotomic/CyclRat.lean

@@ -336,9 +336,9 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     m ∣ f ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ := by
   obtain ⟨i, Hi⟩ := hf
   have hlast :
-    (Fin.castIso (succ_pred_prime hp.out)) (Fin.last (p : ℕ).pred) =
+    (Fin.castOrderIso (succ_pred_prime hp.out)) (Fin.last (p : ℕ).pred) =
     ⟨(p : ℕ).pred, pred_lt hp.out.ne_zero⟩ := Fin.ext rfl
-  have h : ∀ x, (Fin.castIso (succ_pred_prime hp.out)) (Fin.castSuccEmb x) =
+  have h : ∀ x, (Fin.castOrderIso (succ_pred_prime hp.out)) (Fin.castSuccEmb x) =
     ⟨x, lt_trans x.2 (pred_lt hp.out.ne_zero)⟩ := fun x => Fin.ext rfl
   let ζ' := (ζ : L)
   have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
@@ -352,10 +352,10 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     by_contra! habs
     simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt i))] at H
   obtain ⟨y, hy⟩ := hdiv
-  rw [← Equiv.sum_comp (Fin.castIso (succ_pred_prime hp.out)).toEquiv, Fin.sum_univ_castSucc] at hy
+  rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp.out)).toEquiv, Fin.sum_univ_castSucc] at hy
   simp only [hlast, h, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy
   rw [hζ.pow_sub_one_eq hp.out.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib,
-    ← (Fin.castIso hdim).toEquiv.sum_comp] at hy
+    ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy
   simp only [RelIso.coe_fn_toEquiv, Fin.coe_cast, mul_neg, ← Subtype.coe_inj, Fin.coe_castSucc,
     Fin.coe_orderIso_apply] at hy
   push_cast at hy
@@ -371,13 +371,13 @@ theorem dvd_last_coeff_cycl_integer [hp : Fact (p : ℕ).Prime] {ζ : 𝓞 L}
     rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg]
   norm_cast at hy
   rw [sum_sub_distrib] at hy
-  replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨i, hi⟩)) hy
+  replace hy := congr_arg (b.basis.coord ((Fin.castOrderIso hdim.symm) ⟨i, hi⟩)) hy
   rw [← b.basis.equivFun_symm_apply, ← b.basis.equivFun_symm_apply, LinearMap.map_sub,
     b.basis.coord_equivFun_symm, b.basis.coord_equivFun_symm, ← smul_eq_mul,
     ← zsmul_eq_smul_cast] at hy
-  obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.castIso hdim.symm) ⟨i, hi⟩) y m
+  obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.castOrderIso hdim.symm) ⟨i, hi⟩) y m
   rw [hn] at hy
-  simp only [Fin.castIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub,
+  simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Hi, zero_sub,
     neg_eq_iff_eq_neg] at hy
   erw [hy] -- pred vs - 1
   simp [dvd_neg]
@@ -389,9 +389,9 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
   have : Fact (p : ℕ).Prime := ⟨hp⟩
   have hζ' : IsPrimitiveRoot ζ' p := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
   have hcoe : ζ = ⟨ζ', hζ'.isIntegral p.pos⟩ := by rfl
-  have hlast : (Fin.castIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) =
+  have hlast : (Fin.castOrderIso (succ_pred_prime hp)) (Fin.last (p : ℕ).pred) =
       ⟨(p : ℕ).pred, pred_lt hp.ne_zero⟩ := Fin.ext rfl
-  have h : ∀ x, (Fin.castIso (succ_pred_prime hp)) (Fin.castSuccEmb x) =
+  have h : ∀ x, (Fin.castOrderIso (succ_pred_prime hp)) (Fin.castSuccEmb x) =
     ⟨x, lt_trans x.2 (pred_lt hp.ne_zero)⟩ := fun x => Fin.ext rfl
   set b := hζ'.integralPowerBasis' with hb
   have hdim : b.dim = (p : ℕ).pred := by rw [hζ'.power_basis_int'_dim, totient_prime hp,
@@ -404,10 +404,10 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
     by_contra! habs
     simp [le_antisymm habs (le_pred_of_lt (Fin.is_lt j))] at H
   obtain ⟨y, hy⟩ := hdiv
-  rw [← Equiv.sum_comp (Fin.castIso (succ_pred_prime hp)).toEquiv, Fin.sum_univ_castSucc] at hy
+  rw [← Equiv.sum_comp (Fin.castOrderIso (succ_pred_prime hp)).toEquiv, Fin.sum_univ_castSucc] at hy
   simp only [hlast, h, RelIso.coe_fn_toEquiv, Fin.val_mk] at hy
   rw [hζ.pow_sub_one_eq hp.one_lt, ← sum_neg_distrib, smul_sum, sum_range, ← sum_add_distrib,
-    ← (Fin.castIso hdim).toEquiv.sum_comp] at hy
+    ← (Fin.castOrderIso hdim).toEquiv.sum_comp] at hy
   simp only [RelIso.coe_fn_toEquiv, Fin.coe_cast, mul_neg, ← Subtype.coe_inj, Fin.coe_castSucc,
     Fin.coe_orderIso_apply] at hy
   push_cast at hy
@@ -423,10 +423,10 @@ theorem dvd_coeff_cycl_integer (hp : (p : ℕ).Prime) {ζ : 𝓞 L} (hζ : IsPri
     rw [← show ∀ y, _ = _ from fun y => congr_fun b.coe_basis y, ← sub_eq_add_neg]
   norm_cast at hy
   rw [sum_sub_distrib] at hy
-  replace hy := congr_arg (b.basis.coord ((Fin.castIso hdim.symm) ⟨j, hj⟩)) hy
+  replace hy := congr_arg (b.basis.coord ((Fin.castOrderIso hdim.symm) ⟨j, hj⟩)) hy
   rw [← b.basis.equivFun_symm_apply, ← b.basis.equivFun_symm_apply, LinearMap.map_sub,
     b.basis.coord_equivFun_symm, b.basis.coord_equivFun_symm] at hy
-  simp only [Fin.castIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Basis.coord_apply,
+  simp only [Fin.castOrderIso_apply, Fin.cast_mk, Fin.castSucc_mk, Fin.eta, Basis.coord_apply,
     sub_eq_iff_eq_add] at hy
   obtain ⟨n, hn⟩ := b.basis.dvd_coord_smul ((Fin.cast hdim.symm) ⟨j, hj⟩) y m
   rw [hy, ← smul_eq_mul, ← zsmul_eq_smul_cast, ← b.basis.coord_apply, ← Fin.cast_mk, hn]

FltRegular/NumberTheory/Hilbert92.lean

@@ -493,7 +493,7 @@ theorem padicValNat_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℕ) :
 theorem padicValInt_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℤ) :
     (p : ℤ) ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValInt p a := by
   rw [padicValInt, ← Int.natAbs_eq_zero, ← padicValNat_dvd_iff' hp, ← Int.natCast_dvd,
-    Int.coe_nat_pow]
+    Int.natCast_pow]
 
 theorem padicValInt_dvd' {p : ℕ} (a : ℤ) : (p : ℤ) ^ padicValInt p a ∣ a := by
   by_cases hp : p = 1

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "7b3c48b58fa0ae1c8f27889bdb086ea5e4b27b06",
+   "rev": "60d622c124cebcecc000853cdae93f4251f4beb5",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "e8c8a42642ceb5af33708b79ae8a3148b681c236",
+   "rev": "70ec1d99be1e1b835d831f39c01b0d14921d2118",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "35e38eb320982cfd2fcc864e0e0467ca223c8cdb",
+   "rev": "b167323652ab59a5d1b91e906ca4172d1c0474b7",
    "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": "5bf1683fbb7de26aee023022376acb23c740b3f5",
+   "rev": "dbaf55811cc1dd45a83c26c367094da1fe666707",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,