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

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

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

State before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ a.norm
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 ≠ a.norm
Tactic:
apply Ne.symm
State after:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ a.norm ≠ 0

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