awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
    (↑(Finset.range n) : Set ℕ)

Tactic:
exact (Finset.range n).nodup_map_iff_injOn.mp (roots_U_real_nodup n)

Premises used: Iff.mp, Finset.nodup_map_iff_injOn, Polynomial.Chebyshev.roots_U_real_nodup
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k < n
⊢ Multiset.Nodup (α := ℝ)
    (Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n)))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k < n
rw :
  Membership.mem (γ := Multiset ℝ)
    (Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n)))
    (cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
⊢ rootMultiplicity (cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) (U ℝ (↑n : ℤ)) = 1

Tactic:
rw [← count_roots, roots_U_real, Multiset.count_eq_one_of_mem (by simp)]

Premises used: Polynomial.count_roots, Multiset.count_eq_one_of_mem, Polynomial.Chebyshev.roots_U_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hk : k < n
⊢ Membership.mem (γ := Multiset ℝ)
    (Finset.val
      (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
        (Finset.range n)))
    (cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
⊢ 0 < (↑k : ℝ) * π / (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
⊢ 0 < (↑k : ℝ) * π / (↑n : ℝ)

Tactic:
have zero_lt : 0 < k * π / n := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
hc : LT.lt (α := ℝ) 0 (↑n : ℝ)
h : 0 < π
⊢ (↑k : ℝ) * π / (↑n : ℝ) < (↑n : ℝ) * π / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
⊢ (↑k : ℝ) * π / (↑n : ℝ) < π

Tactic:
have lt_pi : k * π / n < π := calc
    k * π / n < n * π / n := by gcongr
    _ = π := mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr hn)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩

Premises used: Iff.mpr, IsLocalMax, isOpen_Ioo, eventually_nhds_iff, And.intro, Exists.intro, OfNat.ofNat, Set.Ioo, Neg.neg, IsMaxFilter
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_1 :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y →
      LE.le (α := ℝ) ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
        ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
refine_2 : -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1
⊢ IsLocalMax (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩

Premises used: Iff.mpr, isOpen_Ioo, eventually_nhds_iff, And.intro, Exists.intro, OfNat.ofNat, Set.Ioo, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
refine_1 : eval x (T ℝ (↑n : ℤ)) ≤ 1
⊢ eval x (T ℝ (↑n : ℤ)) ≤ eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))

Tactic:
rw [(eval_T_real_eq_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]

Premises used: Iff.mpr, le_of_lt, And.intro, Exists.intro, Polynomial.Chebyshev.eval_T_real_eq_one_iff, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ |x| ≤ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ eval x (T ℝ (↑n : ℤ)) ≤ 1

Tactic:
exact (abs_le.mp (abs_eval_T_real_le_one n (by grind))).2

Premises used: abs_le, Polynomial.Chebyshev.abs_eval_T_real_le_one, Nat.cast, And.right, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_2 : cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
rw [← cos_pi]

Premises used: Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi

Premises used: le_refl, Real.pi, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi

Premises used: le_refl, Real.pi, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1

Tactic:
rw [← cos_zero]

Premises used: Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0

Tactic:
cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

Premises used: le_refl, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

Premises used: le_refl, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
⊢ 0 < k

Tactic:
have k_pos : 0 < k := hk₂.pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
⊢ 0 < (↑k : ℝ) * π / (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
⊢ 0 < (↑k : ℝ) * π / (↑n : ℝ)

Tactic:
have zero_lt : 0 < k * π / n := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
hc : LT.lt (α := ℝ) 0 (↑n : ℝ)
h : 0 < π
⊢ (↑k : ℝ) * π / (↑n : ℝ) < (↑n : ℝ) * π / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
⊢ (↑k : ℝ) * π / (↑n : ℝ) < π

Tactic:
have lt_pi : k * π / n < π := calc
    k * π / n < n * π / n := by gcongr
    _ = π := mul_div_cancel_left₀ _ (Nat.cast_ne_zero.mpr hn)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ IsLocalMin (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩

Premises used: Iff.mpr, isOpen_Ioo, IsMinFilter, eventually_nhds_iff, IsLocalMin, And.intro, Exists.intro, OfNat.ofNat, Set.Ioo, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_1 :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y →
      LE.le (α := ℝ) ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ))))
        ((fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) y)
refine_2 : -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))
refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1
⊢ IsLocalMin (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
refine eventually_nhds_iff.mpr ⟨Set.Ioo (-1) 1, ?_, isOpen_Ioo, ?_, ?_⟩

Premises used: Iff.mpr, isOpen_Ioo, eventually_nhds_iff, And.intro, Exists.intro, OfNat.ofNat, Set.Ioo, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
refine_1 : -1 ≤ eval x (T ℝ (↑n : ℤ))
⊢ eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) ≤ eval x (T ℝ (↑n : ℤ))

Tactic:
rw [(eval_T_real_eq_neg_one_iff hn _).mpr ⟨k, le_of_lt hk₁, hk₂, rfl⟩]

Premises used: Iff.mpr, Polynomial.Chebyshev.eval_T_real_eq_neg_one_iff, le_of_lt, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-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
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) x
⊢ -1 ≤ eval x (T ℝ (↑n : ℤ))

Tactic:
refine (abs_le.mp (abs_eval_T_real_le_one n (by grind))).1

Premises used: abs_le, Polynomial.Chebyshev.abs_eval_T_real_le_one, Nat.cast, And.left, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_2 : cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ -1 < cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
rw [← cos_pi]

Premises used: Real.cos_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi

Premises used: le_refl, Real.pi, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos π < cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi

Premises used: le_refl, Real.pi, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
refine_3 : cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < 1

Tactic:
rw [← cos_zero]

Premises used: Real.cos_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0

Tactic:
cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

Premises used: le_refl, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < (↑k : ℝ) * π / (↑n : ℝ)
lt_pi : (↑k : ℝ) * π / (↑n : ℝ) < π
⊢ cos ((↑k : ℝ) * π / (↑n : ℝ)) < cos 0

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_refl 0) (le_of_lt lt_pi) zero_lt

Premises used: le_refl, le_of_lt, Real.cos_lt_cos_of_nonneg_of_le_pi, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
inl : Even k → IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
inr : Odd k → IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (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₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
.inr (isLocalMax_T_real hn hk₀ hk₁ hk₂)

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

Tactic:
exact .inr (isLocalMax_T_real hn hk₀ hk₁ hk₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
h : Even k
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
case inl hk₂ => exact .inr (isLocalMax_T_real hn hk₀ hk₁ hk₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Odd k
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) (cos ((↑k : ℝ) * π / (↑n : ℝ)))

Tactic:
.inl (isLocalMin_T_real hn hk₁ hk₂)

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

Tactic:
exact .inl (isLocalMin_T_real hn hk₁ hk₂)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
mp :
  IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x → ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr :
  (∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))) →
    IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x
⊢ IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x ↔ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : IsLocalExtr (β := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x) 0

Tactic:
replace hx := hx.deriv_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : (↑n : ℝ) * eval x (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ eval x (T ℝ (↑n : ℤ))) x) 0
⊢ eval x (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = 0

Tactic:
rw [Polynomial.deriv, T_derivative_eq_U, eval_mul, Int.cast_natCast, eval_natCast,
      mul_eq_zero_iff_left (by aesop)] at hx

Premises used: Int.cast_natCast, Polynomial.Chebyshev.T_derivative_eq_U, Polynomial.eval_natCast, Polynomial.eval_mul, mul_eq_zero_iff_left, Polynomial.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : eval x (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = 0
⊢ degree (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = (↑(n - 1) : WithBot ℕ)

Tactic:
grind [degree_U_natCast]

Premises used: Polynomial.Chebyshev.degree_U_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : eval x (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1)) = 0
⊢ x ∈ roots (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1))

Tactic:
replace hx : x ∈ (U ℝ (n - 1)).roots :=
      (mem_roots (degree_ne_bot.mp (ne_of_eq_of_ne (by grind [degree_U_natCast])
        (WithBot.natCast_ne_bot (n - 1))))).mpr hx
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : x ∈ roots (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ HSub.hSub (α := ℤ) (↑n : ℤ) 1 = (↑(n - 1) : ℤ)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : x ∈ roots (U ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) 1))
⊢ Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x

Tactic:
rw [show (n - 1 : ℤ) = (n - 1 : ℕ) by grind, roots_U_real, Finset.mem_val] at hx

Premises used: Finset.mem_val, Polynomial.Chebyshev.roots_U_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
mp :
  ∀ (k : ℕ) (hk₁ : k ∈ Finset.range (n - 1))
    (hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x),
    ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

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

Premises used: Finset.mem_image, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ k + 1 < n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
mp : x = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
refine ⟨k + 1, Finset.mem_Ioo.mpr ⟨k.zero_lt_succ, by grind⟩, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
mp : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))
⊢ x = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))

Tactic:
rw [← hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
mp : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 = (↑(k + 1) : ℝ)
mp₁ : HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1 = (↑n : ℝ)
⊢ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = cos ((↑(k + 1) : ℝ) * π / (↑n : ℝ))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
mp mp₁ mp₂ mp₃ : k + 1 = k + 1
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 = (↑(k + 1) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
mp : n - 1 + 1 = n
⊢ HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1 = (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ n - 1 + 1 = n

Tactic:
Nat.sub_add_cancel (Nat.one_le_of_lt hn)

Premises used: Nat.one_le_of_lt, Nat.sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : 2 ≤ n
x : ℝ
hx_1 :
  Membership.mem (γ := Finset ℝ)
    (Finset.image (fun (k : ℕ) ↦ cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1))
      (Finset.range (n - 1)))
    x
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 * π / HAdd.hAdd (α := ℝ) (↑(n - 1) : ℝ) 1) = x
⊢ n - 1 + 1 = n

Tactic:
exact Nat.sub_add_cancel (Nat.one_le_of_lt hn)

Premises used: Nat.one_le_of_lt, Nat.sub_add_cancel