Theorem: Spts.one_lt_of_im_ne_zero (FltRegular/FltThree/Spts.lean)

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

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

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

State before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < a.norm
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 ≠ a.norm

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

State before:
case a
a : ℤ√(-3)
hb : 0 = a.norm
⊢ 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 : a.norm = 0
⊢ -3 < 0
Tactic:
norm_num
State after:
no goals

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

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