Theorem: Spts.ne_zero_of_coprime' (Flt/Spts.lean)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Zsqrtd.norm a ≠ 0
Tactic:
contrapose! hcoprime with H
State after:
a : ℤ√(-3)
H : Zsqrtd.norm a = 0
⊢ ¬IsCoprime a.re a.im

State before:
a : ℤ√(-3)
H : Zsqrtd.norm a = 0
⊢ ¬IsCoprime a.re a.im
Tactic:
obtain ⟨rfl, rfl⟩ := (Zsqrtd.norm_eq_zero_iff (by norm_num) _).mp H
State after:
case refl
H : Zsqrtd.norm 0 = 0
⊢ ¬IsCoprime 0.re 0.im

State before:
case refl
H : Zsqrtd.norm 0 = 0
⊢ ¬IsCoprime 0.re 0.im
Tactic:
exact not_isCoprime_zero_zero
State after:
no goals

State before:
a : ℤ√(-3)
H : Zsqrtd.norm a = 0
⊢ -3 < 0
Tactic:
norm_num
State after:
no goals