awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
k : ℕ
hk : k ∈ Finset.Ioo 0 n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x

Tactic:
rw [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
k : ℕ
hk : k ∈ Finset.Ioo 0 n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
isLocalExtr_T_real (Nat.ne_zero_of_lt hn)
      (Finset.mem_Ioo.mp hk).1 (Finset.mem_Ioo.mp hk).2

Premises used: Finset.mem_Ioo, And.right, And.left, Iff.mp, Nat.ne_zero_of_lt, Polynomial.Chebyshev.isLocalExtr_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
k : ℕ
hk : k ∈ Finset.Ioo 0 n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
exact isLocalExtr_T_real (Nat.ne_zero_of_lt hn)
      (Finset.mem_Ioo.mp hk).1 (Finset.mem_Ioo.mp hk).2

Premises used: Finset.mem_Ioo, And.right, And.left, Iff.mp, Nat.ne_zero_of_lt, Polynomial.Chebyshev.isLocalExtr_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k ≤ n
hk₂ : Even k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ |x| ≤ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k ≤ n
hk₂ : Odd k
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ |x| ≤ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
inl : Even k → IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
inr : Odd k → IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
cases k.even_or_odd

Premises used: Nat.even_or_odd
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
hk₂ : Even k
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
.inr (isMaxOn_T_real hn hk hk₂)

Premises used: IsExtrOn, Polynomial.Chebyshev.isMaxOn_T_real, IsExtrFilter, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
hk₂ : Even k
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
exact .inr (isMaxOn_T_real hn hk hk₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
h : Even k
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
case inl hk₂ => exact .inr (isMaxOn_T_real hn hk hk₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
hk₂ : Odd k
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
.inl (isMinOn_T_real hn hk hk₂)

Premises used: IsExtrOn, Polynomial.Chebyshev.isMinOn_T_real, IsExtrFilter, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk : k ≤ n
hk₂ : Odd k
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
exact .inl (isMinOn_T_real hn hk hk₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
mp :
  IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x →
    ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr :
  (∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))) →
    IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x ↔
    ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
mp : |eval x (T ℝ (↑n : ℤ))| = 1
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
apply (abs_eval_T_real_eq_one_iff hn x).mp

Premises used: Iff.mp, Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ |x| ≤ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
mp : 1 ≤ |eval x (T ℝ (↑n : ℤ))|
⊢ |eval x (T ℝ (↑n : ℤ))| = 1

Tactic:
apply eq_of_le_of_ge (abs_eval_T_real_le_one n (by grind))

Premises used: Polynomial.Chebyshev.abs_eval_T_real_le_one, Nat.cast, eq_of_le_of_ge
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|

Tactic:
h.elim (fun h => ?_) (fun h => ?_)

Premises used: IsExtrOn.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
mp : ∀ (h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x), 1 ≤ |eval x (T ℝ (↑n : ℤ))|
mp₁ : ∀ (h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x), 1 ≤ |eval x (T ℝ (↑n : ℤ))|
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|

Tactic:
refine h.elim (fun h => ?_) (fun h => ?_)

Premises used: IsExtrOn.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|

Tactic:
le_abs.mpr (.inr (le_neg_of_le_neg ?_))

Premises used: Iff.mpr, le_neg_of_le_neg, le_abs, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
mp : eval x (T ℝ (↑n : ℤ)) ≤ -1
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|

Tactic:
refine le_abs.mpr (.inr (le_neg_of_le_neg ?_))

Premises used: Iff.mpr, le_neg_of_le_neg, le_abs, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (cos (1 * π / (↑n : ℝ)))

Tactic:
grind [abs_cos_le_one]

Premises used: Real.abs_cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ eval x (T ℝ (↑n : ℤ)) ≤ eval (cos (1 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))

Tactic:
have := isMinOn_iff.mp h (cos (1 * π / n)) (by grind [abs_cos_le_one])
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : eval x (T ℝ (↑n : ℤ)) ≤ eval (cos (1 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))
⊢ Odd (α := ℕ) 1 ∧ cos (1 * π / (↑n : ℝ)) = cos ((↑1 : ℝ) * π / (↑n : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : eval x (T ℝ (↑n : ℤ)) ≤ eval (cos (1 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))
⊢ eval x (T ℝ (↑n : ℤ)) ≤ -1

Tactic:
rw [(eval_T_real_eq_neg_one_iff hn (cos (1 * π / n))).mpr ⟨1, Nat.one_le_iff_ne_zero.mpr hn,
        by simp⟩] at this

Premises used: Iff.mpr, Real.pi, HMul.hMul, Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff, Real.cos, HDiv.hDiv, Nat.cast, And.intro, Exists.intro, Nat.one_le_iff_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMinOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : eval x (T ℝ (↑n : ℤ)) ≤ -1
⊢ eval x (T ℝ (↑n : ℤ)) ≤ -1

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|

Tactic:
le_abs.mpr (.inl ?_)

Premises used: Iff.mpr, le_abs, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
mp : 1 ≤ eval x (T ℝ (↑n : ℤ))
⊢ 1 ≤ |eval x (T ℝ (↑n : ℤ))|

Tactic:
refine le_abs.mpr (.inl ?_)

Premises used: Iff.mpr, le_abs, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (cos (0 * π / (↑n : ℝ)))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
⊢ eval (cos (0 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))

Tactic:
have := isMaxOn_iff.mp h (cos (0 * π / n)) (by simp)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : eval (cos (0 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))
⊢ 0 ≤ n

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : eval (cos (0 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))
⊢ Even (α := ℕ) 0 ∧ cos (0 * π / (↑n : ℝ)) = cos ((↑0 : ℝ) * π / (↑n : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : eval (cos (0 * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))
⊢ 1 ≤ eval x (T ℝ (↑n : ℤ))

Tactic:
rw [(eval_T_real_eq_one_iff hn _).mpr ⟨0, by simp, by simp⟩] at this

Premises used: Iff.mpr, And.intro, Exists.intro, Polynomial.Chebyshev.eval_T_real_eq_one_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
h_1 : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
h : IsMaxOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x
this : 1 ≤ eval x (T ℝ (↑n : ℤ))
⊢ 1 ≤ eval x (T ℝ (↑n : ℤ))

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
k : ℕ
hk : k ≤ n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) x

Tactic:
rw [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
k : ℕ
hk : k ≤ n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
isExtrOn_T_real hn hk

Premises used: Polynomial.Chebyshev.isExtrOn_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx_1 : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
k : ℕ
hk : k ≤ n
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ IsExtrOn (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (Set.Icc (-1) 1) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
exact isExtrOn_T_real hn hk

Premises used: Polynomial.Chebyshev.isExtrOn_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot : IsRoot (T ℝ (↑n : ℤ)) x
hnz : x ≠ 0
⊢ Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x

Tactic:
rw [← mem_roots (T_ne_zero ℝ n), roots_T_real, Finset.mem_val] at hroot

Premises used: Real, Nat.cast, Polynomial.mem_roots, Polynomial.Chebyshev.roots_T_real, Finset.mem_val, Polynomial.Chebyshev.T_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot : IsRoot (T ℝ (↑n : ℤ)) x
hnz : x ≠ 0
hroot₁ :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
⊢ x ≠ 0

Tactic:
rw [← mem_roots (T_ne_zero ℝ n), roots_T_real, Finset.mem_val] at hroot

Premises used: Real, Nat.cast, Polynomial.mem_roots, Polynomial.Chebyshev.roots_T_real, Finset.mem_val, Polynomial.Chebyshev.T_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
obtain :
  ∀ (k : ℕ) (hk₁ : k ∈ Finset.range n)
    (hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x), Irrational x
⊢ Irrational x

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := Finset.mem_image.mp hroot

Premises used: Finset.mem_image, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
⊢ n ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
⊢ n ≠ 0

Tactic:
have hn : n ≠ 0 := by grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
rw : Irrational (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
⊢ Irrational x

Tactic:
rw [← hk₂]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
⊢ Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
h :
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
    (↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π
⊢ Irrational (cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))

Tactic:
convert! this using 2
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
h :
  (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
    (↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
this : Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
⊢ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) =
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
suffices :
  Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))
⊢ Irrational x

Tactic:
suffices Irrational (cos ((Rat.divInt (2 * k + 1) (2 * n)) * π)) by
    rw [← hk₂]; convert! this using 2; push_cast; field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hr : 3 < (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den
⊢ Irrational (cos ((↑(Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))) : ℝ) * π))

Tactic:
apply irrational_cos_rat_mul_pi

Premises used: irrational_cos_rat_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
hnz : x ≠ 0
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hr : ∀ (hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3), x = 0
⊢ 3 < (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den

Tactic:
contrapose! hnz
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
x : ℝ
hroot :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Finset.range n))
    x
k : ℕ
hk₁ : k ∈ Finset.range n
hk₂ : cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)) = x
hn : n ≠ 0
hnz : (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den ≤ 3
rw :
  (if HMul.hMul (α := ℤ) 2 (↑n : ℤ) = 0 then 1
    else
      (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).natAbs /
        (HMul.hMul (α := ℤ) 2 (↑n : ℤ)).gcd (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1)) =
    2 * n / (2 * n).gcd (2 * k + 1)
⊢ (Rat.divInt (HMul.hMul (α := ℤ) 2 (↑k : ℤ) + 1) (HMul.hMul (α := ℤ) 2 (↑n : ℤ))).den = 2 * n / (2 * n).gcd (2 * k + 1)

Tactic:
rw [Rat.den_divInt]

Premises used: Rat.den_divInt