Theorem: factors2 (Flt/Spts.lean)

State before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
have hparity : Even a.re ↔ Even a.im := by
  simpa [two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
State after:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

State before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ↔ Even a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
simp only [iff_iff_and_or_not_and_not, ← Int.odd_iff_not_even] at hparity
State after:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

State before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hparity : Even a.re ∧ Even a.im ∨ Odd a.re ∧ Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
obtain ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ | ⟨hre, him⟩ := hparity
State after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

case inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

State before:
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
⊢ Even a.re ↔ Even a.im
Tactic:
simpa [two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven
State after:
no goals

State before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
use ⟨c, d⟩
State after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := c, im := d }

State before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := c, im := d }
Tactic:
simp only [Zsqrtd.norm_def, hc, hd]
State after:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)

State before:
case inl.intro.intro.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ (c + c) * (c + c) - -3 * (d + d) * (d + d) = 4 * (c * c - -3 * d * d)
Tactic:
ring
State after:
no goals

State before:
case inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
cases' Int.four_dvd_add_or_sub_of_odd hre him with h4 h4
State after:
case inr.intro.inl
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

case inr.intro.inr
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

State before:
case inr.intro.inl
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
obtain ⟨v, hv⟩ := h4
State after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

State before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
use ⟨v - a.im, v⟩
State after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }

State before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }
Tactic:
rw [eq_comm, ← sub_eq_iff_eq_add] at hv
State after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }

State before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v - a.im, im := v }
Tactic:
simp only [Zsqrtd.norm_def, ← hv]
State after:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (4 * v - a.im) * (4 * v - a.im) - -3 * a.im * a.im = 4 * ((v - a.im) * (v - a.im) - -3 * v * v)

State before:
case inr.intro.inl.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (4 * v - a.im) * (4 * v - a.im) - -3 * a.im * a.im = 4 * ((v - a.im) * (v - a.im) - -3 * v * v)
Tactic:
ring
State after:
no goals

State before:
case inr.intro.inr
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
obtain ⟨v, hv⟩ := h4
State after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b

State before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, Zsqrtd.norm a = 4 * Zsqrtd.norm b
Tactic:
use ⟨v + a.im, v⟩
State after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }

State before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
Tactic:
rw [sub_eq_iff_eq_add] at hv
State after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }

State before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm { re := v + a.im, im := v }
Tactic:
simp only [Zsqrtd.norm_def, hv]
State after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)

State before:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)
Tactic:
ring
State after:
no goals