internlm/Lean-Github huggingface dataset:
Theorem: step1_2
Proof state before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
replace hp : p.norm = 4 := by
  rw [← Zsqrt3.norm_natAbs]
  norm_cast
Proof state after:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Theorem: step1_2
Proof state before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
rw [hp] at hdvd⊢
Proof state after:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Theorem: step1_2
Proof state before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
have heven : Even a.norm :=
  by
  apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
  norm_num
Proof state after:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
heven : Even a.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Theorem: step1_2
Proof state before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
heven : Even a.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
Tactic:
exact step1'' hcoprime hp hq heven
Proof state after:
no goals
Theorem: step1_2
Proof state before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ p.norm = 4
Tactic:
rw [← Zsqrt3.norm_natAbs]
Proof state after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ ↑p.norm.natAbs = 4
Theorem: step1_2
Proof state before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ ↑p.norm.natAbs = 4
Tactic:
norm_cast
Proof state after:
no goals
Theorem: step1_2
Proof state before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ Even a.norm
Tactic:
apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
Proof state after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ 2 ∣ 4
Theorem: step1_2
Proof state before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ 2 ∣ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: step1_2
Proof state before:
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : p.norm.natAbs.Prime
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
rw [← Int.prime_iff_natAbs_prime] at hpprime
Proof state after:
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : Prime p.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Theorem: step1_2
Proof state before:
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : Prime p.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
apply step2 hcoprime hdvd hpprime
Proof state after:
no goals
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
have h2 : 2 < a.norm.natAbs := by
  zify
  rw [abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
  apply lt_of_le_of_ne _ (Spts.not_two _).symm
  rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]
  apply lt_of_le_of_ne _ h2.symm
  rw [← Int.sub_one_lt_iff, sub_self]
  exact Spts.pos_of_coprime' hcoprime
Proof state after:
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
obtain ⟨p, hpdvd, hp⟩ := OddPrimeOrFour.exists_and_dvd h2
Proof state after:
case intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : p ∣ a.norm.natAbs
hp : OddPrimeOrFour p
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : p ∣ a.norm.natAbs
hp : OddPrimeOrFour p
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
rw [← Int.ofNat_dvd_left] at hpdvd
Proof state after:
case intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
obtain ⟨q', hcd, hc, hd⟩ := OddPrimeOrFour.factors a p hcoprime hp hpdvd
Proof state after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : |↑p| = q'.norm
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : |↑p| = q'.norm
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
rw [Nat.abs_cast, ← Zsqrt3.norm_natAbs, Nat.cast_inj] at hcd
Proof state after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
hpdvd : ↑p ∣ a.norm
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
rw [hcd] at hpdvd hp
Proof state after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : ↑q'.norm.natAbs ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : ↑q'.norm.natAbs ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
rw [Int.natAbs_dvd] at hpdvd
Proof state after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp hd
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huv : a = q' * u ∨ a = star q' * u
huvdvd : a.norm = q'.norm * u.norm
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huv : a = q' * u ∨ a = star q' * u
huvdvd : a.norm = q'.norm * u.norm
⊢ ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
use u
Proof state after:
case h
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huv : a = q' * u ∨ a = star q' * u
huvdvd : a.norm = q'.norm * u.norm
⊢ ∃ q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < a.norm.natAbs
Tactic:
zify
Proof state after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < |a.norm|
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < |a.norm|
Tactic:
rw [abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)]
Proof state after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < a.norm
Tactic:
apply lt_of_le_of_ne _ (Spts.not_two _).symm
Proof state after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 ≤ a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 ≤ a.norm
Tactic:
rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]
Proof state after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 < a.norm
Tactic:
apply lt_of_le_of_ne _ h2.symm
Proof state after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 ≤ a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 ≤ a.norm
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
Proof state after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 0 < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 0 < a.norm
Tactic:
exact Spts.pos_of_coprime' hcoprime
Proof state after:
no goals
Theorem: OddPrimeOrFour.factors'
Proof state before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.factors'
Proof state before:
case h.inl
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = q' * u
⊢ ∃ q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
use q'
Proof state after:
case h
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = q' * u
⊢ 0 ≤ q'.re ∧ q'.im ≠ 0 ∧ OddPrimeOrFour q'.norm.natAbs ∧ a = q' * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case h.inr
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ ∃ q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Tactic:
use star q'
Proof state after:
case h
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ 0 ≤ (star q').re ∧
    (star q').im ≠ 0 ∧ OddPrimeOrFour (star q').norm.natAbs ∧ a = star q' * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm
Theorem: OddPrimeOrFour.factors'
Proof state before:
case right
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ u.norm < a.norm
Tactic:
rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← Zsqrt3.norm_natAbs,
  Nat.one_lt_cast]
Proof state after:
case right
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ 1 < q'.norm.natAbs
Theorem: OddPrimeOrFour.factors'
Proof state before:
case right
a : ℤ√(-3)
h2✝ : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < a.norm.natAbs
p : ℕ
q' : ℤ√(-3)
hp : OddPrimeOrFour q'.norm.natAbs
hpdvd : q'.norm ∣ a.norm
hcd : p = q'.norm.natAbs
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : a.norm = q'.norm * u.norm
huv : a = star q' * u
⊢ 1 < q'.norm.natAbs
Tactic:
exact hp.one_lt
Proof state after:
no goals
Theorem: step3
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
suffices
  ∀ n : ℕ,
    a.norm.natAbs = n →
      ∃ f : Multiset (ℤ√(-3)),
        (a = f.prod ∨ a = -f.prod) ∧
          ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
  by exact this a.norm.natAbs rfl
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ ∀ (n : ℕ),
    a.norm.natAbs = n →
      ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ ∀ (n : ℕ),
    a.norm.natAbs = n →
      ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
intro n hn
Proof state after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
n : ℕ
hn : a.norm.natAbs = n
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
n : ℕ
hn : a.norm.natAbs = n
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
induction' n using Nat.strong_induction_on with n ih generalizing a
Proof state after:
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
cases' eq_or_ne a.norm 1 with h h
Proof state after:
case h.inl
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs

case h.inr
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm ≠ 1
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
this :
  ∀ (n : ℕ),
    a.norm.natAbs = n →
      ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
exact this a.norm.natAbs rfl
Proof state after:
no goals
Theorem: step3
Proof state before:
case h.inl
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
use 0
Proof state after:
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ (a = Multiset.prod 0 ∨ a = -Multiset.prod 0) ∧ ∀ pq ∈ 0, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
case h
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ (a = Multiset.prod 0 ∨ a = -Multiset.prod 0) ∧ ∀ pq ∈ 0, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
constructor
Proof state after:
case h.left
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ a = Multiset.prod 0 ∨ a = -Multiset.prod 0

case h.right
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ ∀ pq ∈ 0, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
case h.left
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ a = Multiset.prod 0 ∨ a = -Multiset.prod 0
Tactic:
simp only [Multiset.prod_zero, Spts.eq_one' h]
Proof state after:
no goals
Theorem: step3
Proof state before:
case h.right
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
⊢ ∀ pq ∈ 0, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
intro pq hpq
Proof state after:
case h.right
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
pq : ℤ√(-3)
hpq : pq ∈ 0
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Theorem: step3
Proof state before:
case h.right
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
pq : ℤ√(-3)
hpq : pq ∈ 0
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
Tactic:
exact absurd hpq (Multiset.not_mem_zero _)
Proof state after:
no goals