Theorem: h_lamb_gt_q_sub_one (FormalBook/Chapter_06.lean)

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
let a := lamb.re
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
let b := lamb.im
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
⊢ lamb ∈ primitiveRoots n ℂ → ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
intro h
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have h_lamb: lamb ≠ 1 := by sorry
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have h_a_lt_one: ‖a‖ < 1 := by sorry
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have h_ineq :
    ‖((X - C lamb).eval (q : ℂ))‖^2 > ((q : ℝ) - 1)^2  := by
  calc
    _ = ‖q - lamb‖^2 := by
      simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
    _ = ‖(q : ℂ) - a - I*b‖^2 := by sorry
    _ = ‖(q : ℂ) - a‖^2 + ‖b‖^2 := by sorry
    _ = (q : ℝ)^2 - 2*‖a‖*q + ‖a‖^2 + ‖b‖^2 := by sorry
    _ > ((q : ℝ) - 1)^2 := by sorry
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have : 0 ≤ ((q : ℝ) - 1)^2 := by exact sq_nonneg ((q : ℝ) - 1)
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have g := (Real.sqrt_lt_sqrt_iff this).mpr (h_ineq)
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
have : Real.sqrt (((q:ℝ) - 1) ^ 2) = ((q : ℝ) - 1) := by sorry
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
rw [this] at g
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
rw [norm_eq_abs, Real.sqrt_sq] at g
State after:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < Complex.abs (eval (↑q) (X - C lamb))
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1

R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (Complex.abs (eval (↑q) (X - C lamb)) ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ 0 ≤ Complex.abs (eval (↑q) (X - C lamb))

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
⊢ lamb ≠ 1
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
⊢ ‖a‖ < 1
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
Tactic:
calc
  _ = ‖q - lamb‖^2 := by
    simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
  _ = ‖(q : ℂ) - a - I*b‖^2 := by sorry
  _ = ‖(q : ℂ) - a‖^2 + ‖b‖^2 := by sorry
  _ = (q : ℝ)^2 - 2*‖a‖*q + ‖a‖^2 + ‖b‖^2 := by sorry
  _ > ((q : ℝ) - 1)^2 := by sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖eval (↑q) (X - C lamb)‖ ^ 2 = ‖↑q - lamb‖ ^ 2
Tactic:
simp only [eval_sub, eval_X, eval_C, norm_eq_abs]
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖↑q - lamb‖ ^ 2 = ‖↑q - ↑a - I * ↑b‖ ^ 2
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖↑q - ↑a - I * ↑b‖ ^ 2 = ‖↑q - ↑a‖ ^ 2 + ‖b‖ ^ 2
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ‖↑q - ↑a‖ ^ 2 + ‖b‖ ^ 2 = ↑q ^ 2 - 2 * ‖a‖ * ↑q + ‖a‖ ^ 2 + ‖b‖ ^ 2
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
⊢ ↑q ^ 2 - 2 * ‖a‖ * ↑q + ‖a‖ ^ 2 + ‖b‖ ^ 2 > (↑q - 1) ^ 2
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
⊢ 0 ≤ (↑q - 1) ^ 2
Tactic:
exact sq_nonneg ((q : ℝ) - 1)
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this : 0 ≤ (↑q - 1) ^ 2
g : ((↑q - 1) ^ 2).sqrt < (‖eval (↑q) (X - C lamb)‖ ^ 2).sqrt
⊢ ((↑q - 1) ^ 2).sqrt = ↑q - 1
Tactic:
sorry
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < Complex.abs (eval (↑q) (X - C lamb))
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ ‖eval (↑q) (X - C lamb)‖ > ↑q - 1
Tactic:
exact g
State after:
no goals

State before:
R : Type ?u.6715
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
q n : ℕ
lamb : ℂ
a : ℝ := lamb.re
b : ℝ := lamb.im
h : lamb ∈ primitiveRoots n ℂ
h_lamb : lamb ≠ 1
h_a_lt_one : ‖a‖ < 1
h_ineq : ‖eval (↑q) (X - C lamb)‖ ^ 2 > (↑q - 1) ^ 2
this✝ : 0 ≤ (↑q - 1) ^ 2
g : ↑q - 1 < (Complex.abs (eval (↑q) (X - C lamb)) ^ 2).sqrt
this : ((↑q - 1) ^ 2).sqrt = ↑q - 1
⊢ 0 ≤ Complex.abs (eval (↑q) (X - C lamb))
Tactic:
aesop
State after:
no goals