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

State before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1 ∧ a.im = 0
Tactic:
suffices H : abs a.re = 1
State after:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ abs a.re = 1 ∧ a.im = 0

case H
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1

State before:
case H
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1
Tactic:
contrapose! h
State after:
case H
a : ℤ√(-3)
h : abs a.re ≠ 1
⊢ Zsqrtd.norm a ≠ 1

State before:
case H
a : ℤ√(-3)
h : abs a.re ≠ 1
⊢ Zsqrtd.norm a ≠ 1
Tactic:
cases' lt_or_gt_of_ne h with H H
State after:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ Zsqrtd.norm a ≠ 1

case H.inr
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ Zsqrtd.norm a ≠ 1

State before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ abs a.re = 1 ∧ a.im = 0
Tactic:
refine' ⟨H, _⟩
State after:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ a.im = 0

State before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ a.im = 0
Tactic:
rw [Zsqrtd.norm_def, mul_assoc, ← Int.natAbs_mul_self' a.re, ← Int.abs_eq_natAbs, H, one_mul,
  neg_mul, sub_neg_eq_add, add_right_eq_self, mul_eq_zero, mul_self_eq_zero] at h
State after:
a : ℤ√(-3)
h : 3 = 0 ∨ a.im = 0
H : abs a.re = 1
⊢ a.im = 0

State before:
a : ℤ√(-3)
h : 3 = 0 ∨ a.im = 0
H : abs a.re = 1
⊢ a.im = 0
Tactic:
exact h.resolve_left three_ne_zero
State after:
no goals

State before:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ Zsqrtd.norm a ≠ 1
Tactic:
have : a.re = 0 := by rwa [← Int.abs_lt_one_iff]
State after:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ Zsqrtd.norm a ≠ 1

State before:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ Zsqrtd.norm a ≠ 1
Tactic:
simp only [Zsqrtd.norm_def, this, MulZeroClass.zero_mul, zero_sub, neg_mul, neg_neg]
State after:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ 3 * a.im * a.im ≠ 1

State before:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
by_cases hb : a.im = 0
State after:
case pos
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1

case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 3 * a.im * a.im ≠ 1

State before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ a.re = 0
Tactic:
rwa [← Int.abs_lt_one_iff]
State after:
no goals

State before:
case pos
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
simp only [hb, not_false_iff, zero_ne_one, MulZeroClass.mul_zero]
State after:
no goals

State before:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
have : 1 ≤ abs a.im := by rwa [← Int.abs_lt_one_iff, not_lt] at hb
State after:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 3 * a.im * a.im ≠ 1

State before:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 3 * a.im * a.im ≠ 1
Tactic:
have : 1 ≤ a.im ^ 2 := by
  rw [← sq_abs]
  exact pow_le_pow_of_le_left zero_le_one this 2
State after:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ abs a.im
this : 1 ≤ a.im ^ 2
⊢ 3 * a.im * a.im ≠ 1

State before:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ abs a.im
this : 1 ≤ a.im ^ 2
⊢ 3 * a.im * a.im ≠ 1
Tactic:
linarith
State after:
no goals

State before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 1 ≤ abs a.im
Tactic:
rwa [← Int.abs_lt_one_iff, not_lt] at hb
State after:
no goals

State before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ a.im ^ 2
Tactic:
rw [← sq_abs]
State after:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ abs a.im ^ 2

State before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ abs a.im ^ 2
Tactic:
exact pow_le_pow_of_le_left zero_le_one this 2
State after:
no goals

State before:
case H.inr
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ Zsqrtd.norm a ≠ 1
Tactic:
apply ne_of_gt
State after:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < Zsqrtd.norm a

State before:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < Zsqrtd.norm a
Tactic:
rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add]
State after:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re + 3 * a.im * a.im

State before:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re + 3 * a.im * a.im
Tactic:
apply lt_add_of_lt_of_nonneg
State after:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re

case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * a.im * a.im

State before:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re
Tactic:
rw [← sq, ← sq_abs]
State after:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < abs a.re ^ 2

State before:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < abs a.re ^ 2
Tactic:
exact pow_lt_pow_of_lt_left H zero_le_one zero_lt_two
State after:
no goals

State before:
case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * a.im * a.im
Tactic:
rw [mul_assoc]
State after:
case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * (a.im * a.im)

State before:
case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * (a.im * a.im)
Tactic:
exact mul_nonneg zero_lt_three.le (mul_self_nonneg _)
State after:
no goals