Theorem: Zsqrtd.exists (Flt/Spts.lean)

State before:
d : ℤ
a : ℤ√d
him : a.im ≠ 0
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
cases' le_or_lt a.re 0 with hre hre
State after:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

State before:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
use -a
State after:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ norm a = norm (-a) ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0

State before:
case inl
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : a.re ≤ 0
⊢ norm a = norm (-a) ∧ 0 ≤ (-a).re ∧ (-a).im ≠ 0
Tactic:
simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re,
  and_self_iff, neg_nonneg, Ne.def, not_false_iff, neg_eq_zero]
State after:
no goals

State before:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ ∃ c, norm a = norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0
Tactic:
use a
State after:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ norm a = norm a ∧ 0 ≤ a.re ∧ a.im ≠ 0

State before:
case inr
d : ℤ
a : ℤ√d
him : a.im ≠ 0
hre : 0 < a.re
⊢ norm a = norm a ∧ 0 ≤ a.re ∧ a.im ≠ 0
Tactic:
simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne.def, not_false_iff]
State after:
no goals