Theorem: Spts.ne_zero_of_coprime' (FltRegular/FltThree/Spts.lean)

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

State before:
a : ℤ√(-3)
H : a.norm = 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 (Zsqrtd.re 0) (Zsqrtd.im 0)

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

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