bump

Author: riccardobrasca

FltRegular/FltThree/Edwards.lean

@@ -83,7 +83,6 @@ theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a
   have := hcoprime.isUnit_of_dvd' hre him
   rw [isUnit_iff_dvd_one] at this
   norm_num at this
-  contradiction
 #align step1a step1a
 
 theorem step1 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) :
@@ -158,8 +157,8 @@ theorem step1'' {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hp : p.norm
 
 theorem step2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm ∣ a.norm)
     (hpprime : Prime p.norm) :
-    ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm :=
-  by
+    ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧
+    a.norm = p.norm * u.norm := by
   obtain ⟨u', h, h'⟩ := Spts.mul_of_dvd'' hdvd hpprime
   refine' ⟨u', _, h, h'⟩
   apply Zsqrtd.coprime_of_dvd_coprime hcoprime
@@ -168,23 +167,22 @@ theorem step2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm
 
 theorem step1_2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm ∣ a.norm)
     (hp : OddPrimeOrFour p.norm) (hq : p.im ≠ 0) :
-    ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm :=
-  by
+    ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧
+    a.norm = p.norm * u.norm := by
   obtain hp | ⟨hpprime, -⟩ := hp
   · rw [hp] at hdvd⊢
     have heven : Even a.norm :=
       by
       apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
-      norm_num; decide
+      norm_num
     exact step1'' hcoprime hp hq heven
   · apply step2 hcoprime hdvd hpprime
 #align step1_2 step1_2
 
 theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : a.norm ≠ 1) (hcoprime : IsCoprime a.re a.im) :
     ∃ u q : ℤ√(-3),
       0 ≤ q.re ∧
-        q.im ≠ 0 ∧ OddPrimeOrFour q.norm ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm :=
-  by
+        q.im ≠ 0 ∧ OddPrimeOrFour q.norm ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm := by
   have h2 : 2 < a.norm := by
     apply lt_of_le_of_ne _ (Spts.not_two _).symm
     rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]

FltRegular/FltThree/FltThree.lean

@@ -279,7 +279,7 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
     suffices 3 ∣ 2 * p
       by
       apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
-      norm_num; decide
+      norm_num
     have : 3 ∣ (g : ℤ) := by
       rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
       apply dvd_mul_right
@@ -450,7 +450,7 @@ theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q)
     have : 3 ∣ 2 * p := H.mul_left 2
     have := IsCoprime.isUnit_of_dvd' hgcd ‹_› ‹_›
     rw [isUnit_iff_dvd_one] at this
-    norm_num at this; contradiction
+    norm_num at this
   have not_3_dvd_2 : ¬3 ∣ u - 3 * v := by
     intro hd2
     apply hddd
@@ -586,7 +586,7 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime :
     · zify  at hgcd
       rw [← hgcd]
       exact Int.gcd_dvd_left _ _
-    · norm_num; decide
+    · norm_num
   have h3_ndvd_q : ¬3 ∣ q := by
     intro H
     have := hcoprime.isUnit_of_dvd' h3_dvd_p H

FltRegular/FltThree/OddPrimeOrFour.lean

@@ -42,7 +42,7 @@ theorem OddPrimeOrFour.not_unit {z : ℤ} (h : OddPrimeOrFour z) : ¬IsUnit z :=
   by
   obtain rfl | ⟨h, -⟩ := h
   · rw [isUnit_iff_dvd_one]
-    norm_num; decide
+    norm_num
   · exact h.not_unit
 #align odd_prime_or_four.not_unit OddPrimeOrFour.not_unit
 
@@ -95,7 +95,7 @@ theorem associated_of_dvd {a p : ℤ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFo
     refine' aodd _
     rw [even_iff_two_dvd]
     refine' dvd_trans _ h
-    norm_num; decide
+    norm_num
   · rwa [Prime.dvd_prime_iff_associated pp ap] at h
 #align associated_of_dvd associated_of_dvd
 

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a3b80114adc0948ff493f9acb6ee250f76922d80",
+   "rev": "e403f680f0beb8610c29e6f799132e8be880554e",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "81e04e3518080a288dfa9a490c048e08ab890cb0",
+   "rev": "c26fbb123f5a4e5450ade6106621ace5f5029236",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,