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

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne
State after:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ Zsqrtd.norm a

case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ Zsqrtd.norm a

State before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ Zsqrtd.norm a
Tactic:
apply Zsqrtd.norm_nonneg
State after:
case a.hd
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ -3 ≤ 0

State before:
case a.hd
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals

State before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ Zsqrtd.norm a
Tactic:
apply Ne.symm
State after:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Zsqrtd.norm a ≠ 0

State before:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Zsqrtd.norm a ≠ 0
Tactic:
exact Spts.ne_zero_of_coprime' _ hcoprime
State after:
no goals