bump

.gitignore

@@ -1,3 +1,11 @@
-/build
+# macOS leaves these files everywhere:
+.DS_Store
+# Created by `lake exe cache get` if no home directory is available
+/.cache
+# Prior to v4.3.0-rc2 lake stored files in these locations.
+# We'll leave them in the `.gitignore` for a while for users switching between toolchains.
+/build/
+/lake-packages/
 /lakefile.olean
-/lake-packages/*
+# After v4.3.0-rc2 lake stores its files here:
+/.lake/

FltRegular/CaseI/AuxLemmas.lean

@@ -93,11 +93,11 @@ theorem auxf0k₂ (hp5 : 5 ≤ p) (a b : ℤ) : ∃ i : Fin P, f0k₂ a b (i : 
   refine' ⟨⟨2, two_lt hp5⟩, _⟩
   have h1 : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 1 := by
     intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h
+    simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
   have hzero : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 0 := by
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h
-  simp only [f0k₂, h1, if_false, hzero]
+  simp only [f0k₂, h1, if_false, hzero, one_lt_two.ne']
 
 theorem aux0k₂ {a b : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p) (hab : ¬a ≡ b [ZMOD p])
     {k₁ k₂ : Fin p} (hcong : k₂ ≡ k₁ - 1 [ZMOD p])
@@ -173,12 +173,12 @@ theorem auxf1k₂ (a : ℤ) : ∃ i : Fin P, f1k₂ a (i : ℕ) = 0 := by
   have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 :=
     by
     intro h
-    simp only [Fin.ext_iff, Fin.val_mk] at h
+    simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
   have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 :=
     by
     intro h
     simp only [Fin.ext_iff, Fin.val_mk] at h
-  simp only [f1k₂, h2, if_false, hzero]
+  simp only [f1k₂, h2, if_false, hzero, one_lt_two.ne]
 
 theorem aux1k₂ {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hζ : IsPrimitiveRoot ζ p)
     (caseI : ¬↑p ∣ a * b * c) {k₁ k₂ : Fin p} (hcong : k₂ ≡ k₁ - 1 [ZMOD p])

FltRegular/CaseI/Statement.lean

@@ -133,7 +133,7 @@ theorem exists_ideal {a b c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p)
   simp only [eq_intCast, Int.cast_add, Int.cast_pow] at H₁
   have hζ' := (zeta_spec P ℚ K).unit'_coe
   rw [pow_add_pow_eq_prod_add_zeta_runity_mul
-    (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p ) hζ'] at H₁
+    (hpri.out.eq_two_or_odd.resolve_left fun h => by simp [h] at h5p; contradiction) hζ'] at H₁
   replace H₁ := congr_arg (fun x => span ({ x } : Set R)) H₁
   simp only [← prod_span_singleton, ← span_singleton_pow] at H₁
   refine' Finset.exists_eq_pow_of_mul_eq_pow_of_coprime (fun η₁ hη₁ η₂ hη₂ hη => ?_) H₁ ζ hζ
@@ -182,7 +182,7 @@ theorem ex_fin_div {a b c : ℤ} {ζ : R} (hp5 : 5 ≤ p) (hreg : IsRegularPrime
     intro hP
     rw [← PNat.coe_inj, PNat.mk_coe] at hP
     rw [hP] at hp5
-    simp at hp5
+    contradiction
   haveI := (⟨hpri.out⟩ : Fact (P : ℕ).Prime)
   obtain ⟨u, α, hu⟩ := is_principal hreg hp5 hgcd caseI H hζ
   rw [h, mul_comm _ (↑b : 𝓞 _), ← pow_one hζ'.unit'] at hu

FltRegular/CaseII/AuxLemmas.lean

@@ -100,7 +100,7 @@ lemma ENat.mul_mono_left {k n m : ℕ∞} (hk : k ≠ 0) (hk' : k ≠ ⊤) : k *
     rw [WithTop.mul_top hk]
     simp
   obtain (k|k) := k
-  · simp at hk'
+  · simp at hk'; contradiction
   simp_rw [WithTop.some_eq_coe, ENat.some_eq_coe]
   rw [← ENat.coe_mul, ← ENat.coe_mul, Nat.cast_le, Nat.cast_le]
   refine (strictMono_mul_left_of_pos (Nat.pos_of_ne_zero ?_)).le_iff_le
@@ -132,7 +132,7 @@ theorem isPrincipal_of_isPrincipal_pow_of_Coprime'
     {A K: Type*} [CommRing A] [IsDedekindDomain A] [Fintype (ClassGroup A)]
     [Field K] [Algebra A K] [IsFractionRing A K] (p : ℕ)
     (H : p.Coprime <| Fintype.card <| ClassGroup A) (I : FractionalIdeal A⁰ K)
-    (hI : (I ^ p : Submodule A K).IsPrincipal) : (I : Submodule A K).IsPrincipal := by
+    (hI : (↑(I ^ p) : Submodule A K).IsPrincipal) : (I : Submodule A K).IsPrincipal := by
   by_cases Izero : I = 0
   · rw [Izero, FractionalIdeal.coe_zero]
     exact bot_isPrincipal

FltRegular/CaseII/InductionStep.lean

@@ -19,7 +19,7 @@ local notation "𝔶" => Ideal.span <| singleton y
 local notation "𝔷" => Ideal.span <| singleton z
 local notation "𝔪" => gcd 𝔵 𝔶
 
-variable {m : ℕ} (e : x ^ (p : ℕ) + y ^ (p : ℕ) = ε * (((hζ.unit' : 𝓞 K) - 1) ^ (m + 1) * z) ^ (p : ℕ))
+variable {m : ℕ} (e : x ^ (p : ℕ) + y ^ (p : ℕ) = ε * ((hζ.unit' - 1 : 𝓞 K) ^ (m + 1) * z) ^ (p : ℕ))
 variable (hy : ¬((hζ.unit' : 𝓞 K) - 1 ∣ y)) (hz : ¬((hζ.unit' : 𝓞 K) - 1 ∣ z))
 variable (η : nthRootsFinset p (𝓞 K))
 
@@ -188,7 +188,7 @@ lemma span_pow_add_pow_eq :
 lemma gcd_m_p_pow_eq_one : gcd 𝔪 (𝔭 ^ (m + 1)) = 1 := by
   rw [← Ideal.isCoprime_iff_gcd, IsCoprime.pow_right_iff, Ideal.isCoprime_iff_gcd,
     gcd_zeta_sub_one_eq_one hζ hy]
-  simp only [add_pos_iff, or_true]
+  simp only [add_pos_iff, or_true, one_pos]
 
 lemma m_dvd_z : 𝔪 ∣ 𝔷 := by
   rw [← one_mul 𝔷, ← gcd_m_p_pow_eq_one hζ hy (x := x) (m := m)]
@@ -437,7 +437,7 @@ lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by
   rw [hη, zero_dvd_iff, e] at this
   simp only [mul_eq_zero, Units.ne_zero, PNat.pos,
     pow_eq_zero_iff, add_pos_iff, or_true, false_or] at this
-  rw [this.resolve_left (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt)] at hz
+  rw [this.resolve_left (pow_ne_zero (m + 1) (hζ.unit'_coe.sub_one_ne_zero hpri.out.one_lt))] at hz
   exact hz (dvd_zero _)
 
 lemma stuff (η₁) (hη₁ : η₁ ≠ η₀) (η₂) (hη₂ : η₂ ≠ η₀) :

FltRegular/FltThree/Edwards.lean

@@ -59,6 +59,7 @@ theorem OddPrimeOrFour.factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime
   obtain rfl | ⟨hprime, hodd⟩ := hx
   · refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩
     simp only [Zsqrtd.norm_def, mul_one, abs_of_pos, zero_lt_four, sub_neg_eq_add]
+    decide
   · obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor
     rw [hc]
     apply Zsqrtd.exists c
@@ -73,13 +74,16 @@ theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a
     Odd a.re ∧ Odd a.im :=
   by
   rw [Int.odd_iff_not_even, Int.odd_iff_not_even]
-  have : Even a.re ↔ Even a.im := by simpa [Zsqrtd.norm_def, parity_simps] using heven
+  have : Even a.re ↔ Even a.im := by
+    have : ¬ Even (3 : ℤ) := by decide
+    simpa [this, Zsqrtd.norm_def, parity_simps] using heven
   apply (iff_iff_and_or_not_and_not.mp this).resolve_left
   rw [even_iff_two_dvd, even_iff_two_dvd]
   rintro ⟨hre, him⟩
   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) :
@@ -171,7 +175,7 @@ theorem step1_2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.no
     have heven : Even a.norm :=
       by
       apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
-      norm_num
+      norm_num; decide
     exact step1'' hcoprime hp hq heven
   · apply step2 hcoprime hdvd hpprime
 #align step1_2 step1_2
@@ -418,7 +422,7 @@ theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) :
     apply iff_of_true even_two
     apply ih _ _ huvcoprime rfl
     rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)]
-    norm_num
+    norm_num; decide
   · convert even_zero (α := ℕ)
     simp only [evenFactorExp, Multiset.count_eq_zero, hn]
     contrapose! hparity with hfactor
@@ -516,7 +520,7 @@ theorem step5'
         by
         rw [Nat.even_mul] at this
         apply this.resolve_left
-        norm_num
+        norm_num; decide
       rw [← evenFactorExp.pow r 3, hcube]
       exact factors_2_even' hcoprime
     calc
@@ -579,7 +583,7 @@ theorem step5
   | inr h1 =>
     use -f.prod
     rw [h1, hf, Multiset.prod_nsmul, Odd.neg_pow]
-    norm_num
+    norm_num; decide
 #align step5 step5
 
 theorem step6 (a b r : ℤ) (hcoprime : IsCoprime a b) (hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2) :

FltRegular/FltThree/FltThree.lean

@@ -121,7 +121,8 @@ theorem descent1left {a b c : ℤ} (hapos : a ≠ 0) (h : a ^ 3 + b ^ 3 = c ^ 3)
     exact hapos (pow_eq_zero h)
   have hqnezero : q ≠ 0 := by
     rintro rfl
-    rw [zero_sub, add_zero, Odd.neg_pow (by norm_num), ← sub_eq_add_neg, sub_eq_iff_eq_add] at h
+    rw [zero_sub, add_zero, Odd.neg_pow (by norm_num; decide), ← sub_eq_add_neg,
+      sub_eq_iff_eq_add] at h
     exact flt_not_add_self hpnezero h.symm rfl
   refine' ⟨p, q, hpnezero, hqnezero, _, _, _⟩
   · apply isCoprime_of_dvd _ _ (not_and_of_not_left _ hpnezero)
@@ -225,7 +226,8 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
     have hne2 : d ≠ 2 := by
       rintro rfl
       rw [Nat.cast_two, ← even_iff_two_dvd] at hdright
-      simp [hparity, two_ne_zero, parity_simps] at hdright
+      have : ¬ Even (3 : ℤ) := by decide
+      simp [this, hparity, two_ne_zero, parity_simps] at hdright
     have : 2 < d := lt_of_le_of_ne hdprime.two_le hne2.symm
     have : 3 < d := lt_of_le_of_ne this hne3.symm
     obtain ⟨P, hP⟩ := hdleft
@@ -270,14 +272,14 @@ theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity :
   rw [← pow_mul_pow_sub _ H] at hg
   have : ¬IsUnit (3 : ℤ) := by
     rw [Int.isUnit_iff_natAbs_eq]
-    norm_num
+    norm_num; decide
   apply this
   have hdvdp : 3 ∣ p :=
     by
     suffices 3 ∣ 2 * p
       by
       apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
-      norm_num
+      norm_num; decide
     have : 3 ∣ (g : ℤ) := by
       rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
       apply dvd_mul_right
@@ -325,7 +327,8 @@ theorem obscure' (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity
       · exfalso
         have : Even p := by
           rw [hp']
-          simp [haparity, hbparity, three_ne_zero, parity_simps]
+          have : ¬ Even (9 : ℤ) := by decide
+          simp [this, haparity, hbparity, three_ne_zero, parity_simps]
         have : Even q := by
           rw [hq']
           simp [haparity, hbparity, three_ne_zero, parity_simps]
@@ -341,7 +344,7 @@ theorem Int.cube_of_coprime (a b c s : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc :
     (hcoprimeab : IsCoprime a b) (hcoprimeac : IsCoprime a c) (hcoprimebc : IsCoprime b c)
     (hs : a * b * c = s ^ 3) : ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3 :=
   by
-  have : Odd 3 := by norm_num
+  have : Odd 3 := by decide
   obtain ⟨⟨AB, HAB⟩, ⟨C, HC⟩⟩ :=
     Int.eq_pow_of_mul_eq_pow_odd (IsCoprime.mul_left hcoprimeac hcoprimebc) this hs
   obtain ⟨⟨A, HA⟩, ⟨B, HB⟩⟩ := Int.eq_pow_of_mul_eq_pow_odd hcoprimeab this HAB
@@ -419,7 +422,7 @@ theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q)
   -- 5.
   obtain ⟨r, hr⟩ : ∃ r, 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3 := by
     rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)]
-  have : Odd 3 := by norm_num
+  have : Odd 3 := by decide
   obtain ⟨hcubeleft, hcuberight⟩ := Int.eq_pow_of_mul_eq_pow_odd hgcd this hr
   -- todo shadowing hq
   obtain ⟨u, v, hpfactor, hq, huvcoprime, huvodd⟩ := obscure' p q hp hcoprime hodd hcuberight
@@ -431,8 +434,9 @@ theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q)
     by
     rw [hpfactor]
     ring
-  have : ¬Even (u - 3 * v) := by simp [huvodd, parity_simps]
-  have : ¬Even (u + 3 * v) := by simp [huvodd, parity_simps]
+  have : ¬ Even (3 : ℤ) := by decide
+  have : ¬Even (u - 3 * v) := by simp [‹¬ Even (3 : ℤ)›, huvodd, parity_simps]
+  have : ¬Even (u + 3 * v) := by simp [‹¬ Even (3 : ℤ)›, huvodd, parity_simps]
   have notdvd_2_2 : ¬2 ∣ u - 3 * v := by
     rw [← even_iff_two_dvd]
     exact ‹¬Even (u - 3 * v)›
@@ -446,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
+    norm_num at this; contradiction
   have not_3_dvd_2 : ¬3 ∣ u - 3 * v := by
     intro hd2
     apply hddd
@@ -465,11 +469,11 @@ theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q)
     · apply mul_ne_zero two_ne_zero u_ne_zero
     · rw [sub_ne_zero]
       rintro rfl
-      simp only [false_or_iff, iff_not_self, parity_simps] at huvodd
+      simp only [‹¬ Even (3 : ℤ)›, false_or_iff, iff_not_self, parity_simps] at huvodd
     · intro H
       rw [add_eq_zero_iff_eq_neg] at H
       apply iff_not_self
-      simpa [H, parity_simps] using huvodd
+      simpa [‹¬ Even (3 : ℤ)›, H, parity_simps] using huvodd
     · apply Int.gcd1_coprime12 u v <;> assumption
     · apply Int.gcd1_coprime13 u v <;> assumption
     · apply Int.gcd1_coprime23 u v <;> assumption
@@ -539,7 +543,8 @@ theorem descent_gcd3_coprime {q s : ℤ} (h3_ndvd_q : ¬3 ∣ q) (hspos : s ≠
   have h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2 :=
     by
     rw [← even_iff_two_dvd]
-    simp [two_ne_zero, hodd', parity_simps]
+    have : ¬ Even (3 : ℤ) := by decide
+    simp [this, two_ne_zero, hodd', parity_simps]
   have h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2 := by
     intro H
     apply h3_ndvd_q
@@ -581,12 +586,12 @@ 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
+    · norm_num; decide
   have h3_ndvd_q : ¬3 ∣ q := by
     intro H
     have := hcoprime.isUnit_of_dvd' h3_dvd_p H
     rw [Int.isUnit_iff_natAbs_eq] at this
-    norm_num at this
+    norm_num at this; contradiction
   -- 2.
   obtain ⟨s, rfl⟩ := h3_dvd_p
   have hspos : s ≠ 0 := right_ne_zero_of_mul hp
@@ -604,14 +609,15 @@ theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime :
   have hodd' : Even q ↔ ¬Even s :=
     by
     rw [Iff.comm, not_iff_comm, Iff.comm]
-    simpa [parity_simps] using hodd
+    have : ¬ Even (3 : ℤ) := by decide
+    simpa [this, parity_simps] using hodd
   have hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2) :=
     descent_gcd3_coprime h3_ndvd_q hspos hcoprime' hodd'
   -- 4.
   obtain ⟨r, hr⟩ : ∃ r, 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = r ^ 3 := by
     rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)]
   rw [hps] at hr
-  have : Odd 3 := by norm_num
+  have : Odd 3 := by norm_num; decide
   obtain ⟨hcubeleft, hcuberight⟩ := Int.eq_pow_of_mul_eq_pow_odd hcoprime'' this hr
   -- 5.
   -- todo shadows hq hq

FltRegular/FltThree/OddPrimeOrFour.lean

@@ -31,7 +31,7 @@ theorem OddPrimeOrFour.one_lt_abs {z : ℤ} (h : OddPrimeOrFour z) : 1 < abs z :
   by
   obtain rfl | ⟨h, -⟩ := h
   · rw [Int.abs_eq_natAbs]
-    norm_num
+    norm_num; decide
   · rw [Int.abs_eq_natAbs]
     rw [Int.prime_iff_natAbs_prime] at h
     norm_cast
@@ -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
+    norm_num; decide
   · 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
+    norm_num; decide
   · rwa [Prime.dvd_prime_iff_associated pp ap] at h
 #align associated_of_dvd associated_of_dvd
 
@@ -166,8 +166,7 @@ theorem oddFactors.zero : oddFactors 0 = 0 :=
 #align odd_factors.zero oddFactors.zero
 
 theorem oddFactors.not_two_mem (x : ℤ) : (2 : ℤ) ∉ oddFactors x := by
-  simp only [oddFactors, even_bit0, not_true, not_false_iff, Int.odd_iff_not_even, and_false_iff,
-    Multiset.mem_filter]
+  simp [oddFactors]
 #align odd_factors.not_two_mem oddFactors.not_two_mem
 
 theorem oddFactors.nonneg {z a : ℤ} (ha : a ∈ oddFactors z) : 0 ≤ a :=

FltRegular/FltThree/Primes.lean

@@ -25,7 +25,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) :
   by
   have h0' : x ≠ 0 := by
     rintro rfl
-    simp only at hodd 
+    contradiction
   set c := a % x with hc
   by_cases H : 2 * c.natAbs < x.natAbs
   · exact ⟨a / x, c, Int.emod_add_ediv' a x, H⟩
@@ -56,7 +56,7 @@ nonrec theorem Int.two_not_cube (r : ℤ) : r ^ 3 ≠ 2 :=by
   intro H
   apply two_not_cube r.natAbs
   rw [← Int.natAbs_pow, H]
-  norm_num
+  norm_num; decide
 #align int.two_not_cube Int.two_not_cube  
 
 -- todo square neg_square and neg_pow_bit0

FltRegular/FltThree/Spts.lean

@@ -22,7 +22,8 @@ theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) :
 theorem factors2 {a : ℤ√(-3)} (heven : Even a.norm) : ∃ b : ℤ√(-3), a.norm = 4 * b.norm :=
   by
   have hparity : Even a.re ↔ Even a.im := by
-    simpa [two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
+    have : ¬ Even (3 : ℤ) := by decide
+    simpa [this, two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
   simp only [iff_iff_and_or_not_and_not, ← Int.odd_iff_not_even] at hparity
   obtain ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ | ⟨hre, him⟩ := hparity
   · use ⟨c, d⟩
@@ -138,7 +139,7 @@ theorem factors' (a : ℤ√(-3)) (f : ℤ) (g : ℤ) (hodd : Odd f) (hgpos : g
     refine' IH g'.natAbs _ c g' hg'pos _ _ rfl
     · rw [Int.natAbs_mul]
       apply lt_mul_of_one_lt_left (Int.natAbs_pos.mpr hg'pos)
-      norm_num
+      norm_num; decide
     · rw [← mul_right_inj' (four_ne_zero' ℤ), ← hc, ← hfactor, mul_left_comm]
     · intro f' hf'dvd hf'odd
       refine' hnotform f' _ hf'odd
@@ -329,7 +330,7 @@ theorem Spts.eq_one {a : ℤ√(-3)} (h : a.norm = 1) : abs a.re = 1 ∧ a.im =
   · have : a.re = 0 := by rwa [← Int.abs_lt_one_iff]
     simp only [Zsqrtd.norm_def, this, MulZeroClass.zero_mul, zero_sub, neg_mul, neg_neg]
     by_cases hb : a.im = 0
-    · simp only [hb, not_false_iff, zero_ne_one, MulZeroClass.mul_zero]
+    · simp [hb]
     · have : 1 ≤ abs a.im := by rwa [← Int.abs_lt_one_iff, not_lt] at hb
       have : 1 ≤ a.im ^ 2 := by
         rw [← sq_abs]