Theorem: Spts.one_lt_of_im_ne_zero (Flt/Spts.lean)

State before:
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne
State after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≤ Zsqrtd.norm a

case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≠ Zsqrtd.norm a

State before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≤ Zsqrtd.norm a
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
State after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < Zsqrtd.norm a

State before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a)
State after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 ≠ Zsqrtd.norm a

State before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 ≠ Zsqrtd.norm a
Tactic:
contrapose! hb
State after:
case a
a : ℤ√(-3)
hb : 0 = Zsqrtd.norm a
⊢ a.im = 0

State before:
case a
a : ℤ√(-3)
hb : 0 = Zsqrtd.norm a
⊢ a.im = 0
Tactic:
rw [eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num) a] at hb
State after:
case a
a : ℤ√(-3)
hb : a = 0
⊢ a.im = 0

State before:
case a
a : ℤ√(-3)
hb : a = 0
⊢ a.im = 0
Tactic:
rw [hb, Zsqrtd.zero_im]
State after:
no goals

State before:
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals

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

State before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≠ Zsqrtd.norm a
Tactic:
intro H
State after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
H : 1 = Zsqrtd.norm a
⊢ False

State before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
H : 1 = Zsqrtd.norm a
⊢ False
Tactic:
exact hb (Spts.eq_one H.symm).2
State after:
no goals