Theorem: factors2 (FltRegular/FltThree/Spts.lean)

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

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

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

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

State before:
a : ℤ√(-3)
heven : Even a.norm
⊢ Even a.re ↔ Even a.im
Tactic:
have : ¬ Even (3 : ℤ) := by decide
State after:
a : ℤ√(-3)
heven : Even a.norm
this : ¬Even 3
⊢ Even a.re ↔ Even a.im

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

State before:
a : ℤ√(-3)
heven : Even a.norm
⊢ ¬Even 3
Tactic:
decide
State after:
no goals

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

State before:
case h
a : ℤ√(-3)
heven : Even a.norm
c : ℤ
hc : a.re = c + c
d : ℤ
hd : a.im = d + d
⊢ a.norm = 4 * { re := c, im := d }.norm
Tactic:
simp only [Zsqrtd.norm_def, hc, hd]
State after:
case h
a : ℤ√(-3)
heven : Even a.norm
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 h
a : ℤ√(-3)
heven : Even a.norm
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 a.norm
hre : Odd a.re
him : Odd a.im
⊢ ∃ b, a.norm = 4 * b.norm
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 a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re + a.im
⊢ ∃ b, a.norm = 4 * b.norm

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

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

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

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

State before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm
Tactic:
simp only [Zsqrtd.norm_def, ← hv]
State after:
case h
a : ℤ√(-3)
heven : Even a.norm
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 h
a : ℤ√(-3)
heven : Even a.norm
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 a.norm
hre : Odd a.re
him : Odd a.im
h4 : 4 ∣ a.re - a.im
⊢ ∃ b, a.norm = 4 * b.norm
Tactic:
obtain ⟨v, hv⟩ := h4
State after:
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re - a.im = 4 * v
⊢ ∃ b, a.norm = 4 * b.norm

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

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

State before:
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ a.norm = 4 * { re := v + a.im, im := v }.norm
Tactic:
simp only [Zsqrtd.norm_def, hv]
State after:
case h
a : ℤ√(-3)
heven : Even a.norm
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 h
a : ℤ√(-3)
heven : Even a.norm
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