Theorem: OddPrimeOrFour.factors' (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
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]
  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✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
obtain ⟨p, hpdvd, hp⟩ := OddPrimeOrFour.exists_and_dvd h2
State after:
case intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
obtain ⟨q', hcd, hc, hd⟩ := OddPrimeOrFour.factors a p hcoprime hp hpdvd
State after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
rw [← abs_dvd, hcd] at hpdvd
State after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
have hp' := hp.abs
State after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Abs.abs p)
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Abs.abs p)
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
rw [hcd] at hp'
State after:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
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✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huv : a = q' * u ∨ a = star q' * u
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huv : a = q' * u ∨ a = star q' * u
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
⊢ ∃ u q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
use u
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huv : a = q' * u ∨ a = star q' * u
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
⊢ ∃ q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne _ (Spts.not_two _).symm
State after:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 ≤ Zsqrtd.norm a

State before:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 2 ≤ Zsqrtd.norm a
Tactic:
rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff]
State after:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 < Zsqrtd.norm a

State before:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne _ h2.symm
State after:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 ≤ Zsqrtd.norm a

State before:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 1 ≤ Zsqrtd.norm a
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
State after:
a : ℤ√(-3)
h2 : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
⊢ 0 < Zsqrtd.norm a

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

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = q' * u
⊢ ∃ q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
use q'
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = q' * u
⊢ 0 ≤ q'.re ∧
    q'.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q') ∧ a = q' * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.inr
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = star q' * u
⊢ ∃ q,
    0 ≤ q.re ∧
      q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
use star q'
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.inr
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = star q' * u
⊢ 0 ≤ (star q').re ∧
    (star q').im ≠ 0 ∧
      OddPrimeOrFour (Zsqrtd.norm (star q')) ∧ a = star q' * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.inr
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = star q' * u
⊢ Zsqrtd.norm u < Zsqrtd.norm a
Tactic:
rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← hcd]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.inr
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = star q' * u
⊢ 1 < Abs.abs p

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.inr
a : ℤ√(-3)
h2✝ : Zsqrtd.norm a ≠ 1
hcoprime : IsCoprime a.re a.im
h2 : 2 < Zsqrtd.norm a
p : ℤ
hpdvd✝ : p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour p
q' : ℤ√(-3)
hpdvd : Zsqrtd.norm q' ∣ Zsqrtd.norm a
hcd : Abs.abs p = Zsqrtd.norm q'
hc : 0 ≤ q'.re
hd : q'.im ≠ 0
hp' : OddPrimeOrFour (Zsqrtd.norm q')
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvdvd : Zsqrtd.norm a = Zsqrtd.norm q' * Zsqrtd.norm u
huv : a = star q' * u
⊢ 1 < Abs.abs p
Tactic:
exact hp.one_lt_abs
State after:
no goals