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

State before:
a : ℤ√(-3)
⊢ Zsqrtd.norm a ≠ 2
Tactic:
rw [Zsqrtd.norm_def]
State after:
a : ℤ√(-3)
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2

State before:
a : ℤ√(-3)
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
obtain him | him := eq_or_ne a.im 0
State after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2

case inr
a : ℤ√(-3)
him : a.im ≠ 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2

State before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq]
State after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(Int.natAbs a.re ^ 2) ≠ 2

State before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(Int.natAbs a.re ^ 2) ≠ 2
Tactic:
norm_cast
State after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ¬Int.natAbs a.re ^ 2 = 2

State before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ¬Int.natAbs a.re ^ 2 = 2
Tactic:
apply (Nat.pow_left_strictMono one_le_two).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num
State after:
no goals

State before:
case inr
a : ℤ√(-3)
him : a.im ≠ 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
apply ne_of_gt
State after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < a.re * a.re - -3 * a.im * a.im

State before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < a.re * a.re - -3 * a.im * a.im
Tactic:
apply lt_add_of_nonneg_of_lt (mul_self_nonneg a.re)
State after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < -(-3 * a.im * a.im)

State before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 < -(-3 * a.im * a.im)
Tactic:
rw [← Int.add_one_le_iff]
State after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ -(-3 * a.im * a.im)

State before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ -(-3 * a.im * a.im)
Tactic:
rw [mul_assoc, neg_mul_eq_neg_mul, neg_neg]
State after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ 3 * (a.im * a.im)

State before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 2 + 1 ≤ 3 * (a.im * a.im)
Tactic:
refine' le_mul_of_one_le_right zero_lt_three.le _
State after:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 1 ≤ a.im * a.im

State before:
case inr.h
a : ℤ√(-3)
him : a.im ≠ 0
⊢ 1 ≤ a.im * a.im
Tactic:
rwa [← Int.sub_one_lt_iff, sub_self, mul_self_pos]
State after:
no goals