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

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
Tactic:
refine' ⟨_, hq⟩
State after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = 1
Tactic:
calc
  p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by rw [hq, mul_one, add_sub_cancel]
  _ = p.norm - 3 := by
    rw [Zsqrtd.norm_def]
    ring
  _ = 1 := by
    rw [hfour]
    norm_num
State after:
no goals

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
⊢ p.im ^ 2 = 1 → abs p.im = 1
Tactic:
intro h
State after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ abs p.im = 1

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
this : p.re ^ 2 = 1 ∧ p.im ^ 2 = 1
h : p.im ^ 2 = 1
⊢ abs p.im = 1
Tactic:
rwa [← sq_eq_sq (abs_nonneg (_ : ℤ)) zero_le_one, one_pow, sq_abs]
State after:
no goals

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 = 1
Tactic:
apply le_antisymm
State after:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1

case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2

State before:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ p.im ^ 2 ≤ 1
Tactic:
contrapose! hfour with hq'
State after:
case a
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ Zsqrtd.norm p ≠ 4

State before:
case a
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ Zsqrtd.norm p ≠ 4
Tactic:
apply ne_of_gt
State after:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ 4 < Zsqrtd.norm p

State before:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 < p.im ^ 2
⊢ 4 < Zsqrtd.norm p
Tactic:
rw [← Int.add_one_le_iff] at hq'
State after:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < Zsqrtd.norm p

State before:
case a.h
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < Zsqrtd.norm p
Tactic:
calc
  4 < 3 * 2 := by norm_num
  _ ≤ 3 * p.im ^ 2 := (Int.mul_le_mul_of_nonneg_left hq' (by norm_num))
  _ ≤ p.re ^ 2 + 3 * p.im ^ 2 := (le_add_of_nonneg_left (pow_two_nonneg p.re))
  _ = p.norm := by
    rw [Zsqrtd.norm_def]
    ring
State after:
no goals

State before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 4 < 3 * 2
Tactic:
norm_num
State after:
no goals

State before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ 0 ≤ 3
Tactic:
norm_num
State after:
no goals

State before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = Zsqrtd.norm p
Tactic:
rw [Zsqrtd.norm_def]
State after:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = p.re * p.re - -3 * p.im * p.im

State before:
p : ℤ√(-3)
hq : p.im ≠ 0
hq' : 1 + 1 ≤ p.im ^ 2
⊢ p.re ^ 2 + 3 * p.im ^ 2 = p.re * p.re - -3 * p.im * p.im
Tactic:
ring
State after:
no goals

State before:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 1 ≤ p.im ^ 2
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
State after:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 0 < p.im ^ 2

State before:
case a
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq : p.im ≠ 0
⊢ 0 < p.im ^ 2
Tactic:
exact sq_pos_of_ne_zero _ hq
State after:
no goals

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3
Tactic:
rw [hq, mul_one, add_sub_cancel]
State after:
no goals

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = Zsqrtd.norm p - 3
Tactic:
rw [Zsqrtd.norm_def]
State after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ p.re ^ 2 + 3 * p.im ^ 2 - 3 = p.re * p.re - -3 * p.im * p.im - 3
Tactic:
ring
State after:
no goals

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ Zsqrtd.norm p - 3 = 1
Tactic:
rw [hfour]
State after:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ 4 - 3 = 1

State before:
p : ℤ√(-3)
hfour : Zsqrtd.norm p = 4
hq✝ : p.im ≠ 0
hq : p.im ^ 2 = 1
⊢ 4 - 3 = 1
Tactic:
norm_num
State after:
no goals