Theorem: OddPrimeOrFour.factors' (FltRegular/FltThree/Edwards.lean)

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

State before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < a.norm.natAbs
Tactic:
zify
State after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < |a.norm|

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)]
State after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < a.norm

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
State after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 ≤ a.norm

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]
State after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 < a.norm

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
State after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 ≤ a.norm

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]
State after:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 0 < a.norm

State before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 0 < a.norm
Tactic:
exact Spts.pos_of_coprime' hcoprime
State after:
no goals

State before:
a : ℤ√(-3)
h2 : a.norm ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals

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'
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

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'
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

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]
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

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
State after:
no goals