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

State before:
a : ℤ√(-3)
h : a.norm = 1
⊢ |a.re| = 1 ∧ a.im = 0
Tactic:
suffices H : abs a.re = 1 by
  refine' ⟨H, _⟩
  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
  exact h.resolve_left three_ne_zero
State after:
a : ℤ√(-3)
h : a.norm = 1
⊢ |a.re| = 1

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

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

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

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

State before:
a : ℤ√(-3)
h : a.norm = 1
H : |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 : |a.re| = 1
⊢ a.im = 0

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

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

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

State before:
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1

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

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

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

State before:
case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 3 * a.im * a.im ≠ 1

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

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

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

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

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

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

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

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

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

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

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

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

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