bump mathlib

Author: kbuzzard

FLT/Basic/Reductions.lean

@@ -175,15 +175,15 @@ lemma aux₁.ha4 (hab : gcd a₁ b₁ = 1) : ((aux₁ a₁ b₁ c₁).1 : ZMod 4
       exact a3mod4
     · rename_i _ a1mod4
       have foo : 2 ∣ b₁ := by
-        exact (ZMod.int_cast_zmod_eq_zero_iff_dvd b₁ 2).mp b_even
+        exact (ZMod.intCast_zmod_eq_zero_iff_dvd b₁ 2).mp b_even
       have bar : ¬ 2 ∣ a₁ := by
         intro h
         apply aux _ h foo
         rename_i x x_1
         simp_all only [ne_eq, Fin.zero_eta, gcd_eq_zero_iff, false_and, not_false_eq_true]
       -- want to do fin_cases on (-a₁ : ZMod 4)
       rcases ZMod4cases (-a₁ : ℤ) with (h | h | h | h)
-      · rw [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h
+      · rw [ZMod.intCast_zmod_eq_zero_iff_dvd] at h
         simp only [Nat.cast_ofNat, dvd_neg] at h
         exfalso
         apply bar
@@ -198,7 +198,7 @@ lemma aux₁.ha4 (hab : gcd a₁ b₁ = 1) : ((aux₁ a₁ b₁ c₁).1 : ZMod 4
         apply bar
         simp only [Int.cast_neg, ← add_eq_zero_iff_neg_eq] at h
         have foo : ((a₁ + 2 : ℤ) : ZMod 4) = 0 := by assumption_mod_cast
-        rw [ZMod.int_cast_zmod_eq_zero_iff_dvd] at foo
+        rw [ZMod.intCast_zmod_eq_zero_iff_dvd] at foo
         rw [← dvd_add_left (c := 2) (by norm_num)]
         refine dvd_trans ?_ foo
         norm_num
@@ -211,11 +211,11 @@ lemma aux₁.ha4 (hab : gcd a₁ b₁ = 1) : ((aux₁ a₁ b₁ c₁).1 : ZMod 4
       · rename_i _ b1mod4
         -- now need to check a
         rcases ZMod4cases b₁ with (h | h | h | h)
-        · rw [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h
+        · rw [ZMod.intCast_zmod_eq_zero_iff_dvd] at h
           simp only [Nat.cast_ofNat, dvd_neg] at h
           exfalso
           apply hb1
-          simp only [Fin.zero_eta, ZMod.int_cast_zmod_eq_zero_iff_dvd]
+          simp only [Fin.zero_eta, ZMod.intCast_zmod_eq_zero_iff_dvd]
           refine dvd_trans ?_ h
           norm_num
         · simp [h]
@@ -224,8 +224,8 @@ lemma aux₁.ha4 (hab : gcd a₁ b₁ = 1) : ((aux₁ a₁ b₁ c₁).1 : ZMod 4
           have foo : ((b₁ - 2 : ℤ) : ZMod 4) = 0 := by assumption_mod_cast
           exfalso
           apply hb1
-          rw [ZMod.int_cast_zmod_eq_zero_iff_dvd] at foo
-          apply (ZMod.int_cast_zmod_eq_zero_iff_dvd _ 2).2
+          rw [ZMod.intCast_zmod_eq_zero_iff_dvd] at foo
+          apply (ZMod.intCast_zmod_eq_zero_iff_dvd _ 2).2
           rw [← dvd_sub_left (c := 2) (by norm_num)]
           refine dvd_trans ?_ foo
           norm_num
@@ -239,19 +239,19 @@ lemma aux₁.ha4 (hab : gcd a₁ b₁ = 1) : ((aux₁ a₁ b₁ c₁).1 : ZMod 4
         · exfalso
           apply a_odd
           change _ = 0
-          rw [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h ⊢
+          rw [ZMod.intCast_zmod_eq_zero_iff_dvd] at h ⊢
           refine dvd_trans ?_ h
           norm_num
         · simp [h]
           decide
         · exfalso
           apply a_odd
           change _ = 0
-          rw [ZMod.int_cast_zmod_eq_zero_iff_dvd]
+          rw [ZMod.intCast_zmod_eq_zero_iff_dvd]
           rw [← dvd_sub_left (c := 2) (by norm_num)]
           rw [← sub_eq_zero] at h
           have foo : ((a₁ - 2 : ℤ) : ZMod 4) = 0 := by assumption_mod_cast
-          rw [ZMod.int_cast_zmod_eq_zero_iff_dvd] at foo
+          rw [ZMod.intCast_zmod_eq_zero_iff_dvd] at foo
           refine dvd_trans ?_ foo
           norm_num
         · exfalso
@@ -310,21 +310,21 @@ lemma gcdab_eq_gcdac {a b c : ℤ} {p : ℕ} (hp : 0 < p) (h : a ^ p + b ^ p = c
     gcd a b = gcd a c := by
   have foo : gcd a b ∣ gcd a c := by
     apply dvd_gcd (gcd_dvd_left a b)
-    rw [← Int.pow_dvd_pow_iff hp, ← h]
+    rw [← Int.pow_dvd_pow_iff hp.ne', ← h]
     apply dvd_add
-    · rw [Int.pow_dvd_pow_iff hp]
+    · rw [Int.pow_dvd_pow_iff hp.ne']
       exact gcd_dvd_left a b
-    · rw [Int.pow_dvd_pow_iff hp]
+    · rw [Int.pow_dvd_pow_iff hp.ne']
       exact gcd_dvd_right a b
   have bar : gcd a c ∣ gcd a b := by
     apply dvd_gcd (gcd_dvd_left a c)
     have h2 : b ^ p = c ^ p - a ^ p := eq_sub_of_add_eq' h
-    rw [← Int.pow_dvd_pow_iff hp, h2]
+    rw [← Int.pow_dvd_pow_iff hp.ne', h2]
     apply dvd_add
-    · rw [Int.pow_dvd_pow_iff hp]
+    · rw [Int.pow_dvd_pow_iff hp.ne']
       exact gcd_dvd_right a c
     · rw [dvd_neg]
-      rw [Int.pow_dvd_pow_iff hp]
+      rw [Int.pow_dvd_pow_iff hp.ne']
       exact gcd_dvd_left a c
   change _ ∣ (Int.gcd a c : ℤ) at foo
   apply Int.ofNat_dvd.1 at bar

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "f3447c3732c9d6e8df3bdad78e5ecf7e8b353bbc",
+   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
+   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "8be30c25e3caa06937feeb62f7ca898370f80ee9",
+   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
    "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": "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": "32531f6a61daf705cf6b38726b3c2ac5bcc553d1",
+   "rev": "919a721fa2a6ad2997a95e3337c88845b5936e44",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0-rc2
+leanprover/lean4:v4.7.0