awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ (↑n : ℤ))| = 1
⊢ |x| ≤ 1

Tactic:
have hx := (abs_eval_T_real_le_one_iff (Nat.cast_ne_zero.mpr hn) x).mpr (le_of_eq hTx)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ (↑n : ℤ))| = 1
hx : |x| ≤ 1
⊢ ∃ (k : ℤ), (↑k : ℝ) * π = (↑n : ℝ) * arccos x

Tactic:
rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx

Premises used: Int.cast_natCast, Polynomial.Chebyshev.T_real_cos, le_of_max_le_left, Real.cos_arccos, neg_le_of_abs_le, Real.abs_cos_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : |eval x (T ℝ (↑n : ℤ))| = 1
hx : |x| ≤ 1
hTx₁ : ∃ (k : ℤ), (↑k : ℝ) * π = (↑n : ℝ) * arccos x
⊢ |x| ≤ 1

Tactic:
rw [← cos_arccos (neg_le_of_abs_le hx) (le_of_max_le_left hx), T_real_cos,
      Int.cast_natCast, abs_cos_eq_one_iff] at hTx

Premises used: Int.cast_natCast, Polynomial.Chebyshev.T_real_cos, le_of_max_le_left, Real.cos_arccos, neg_le_of_abs_le, Real.abs_cos_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hTx : ∃ (k : ℤ), (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hx : |x| ≤ 1
mp : ∀ (k : ℤ) (hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x), ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
obtain ⟨k, hk⟩ := hTx
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
⊢ (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)

Tactic:
simpa [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
⊢ (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)

Tactic:
have hk' : k = n * (arccos x / π) := by simpa [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
rw : 0 ≤ (↑n : ℝ) * (arccos x / π)
⊢ 0 ≤ k

Tactic:
rw [← Int.cast_nonneg_iff (R := ℝ), hk']

Premises used: Int.cast_nonneg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
positivity positivity₁ positivity₂ positivity₃ : 0 ≤ arccos x → 0 ≤ (↑n : ℝ) * (arccos x / π)
⊢ 0 ≤ (↑n : ℝ) * (arccos x / π)

Tactic:
positivity [arccos_nonneg x]

Premises used: Real.arccos_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℤ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
mp :
  ∀ (k : ℕ) (hk : (↑(↑k : ℤ) : ℝ) * π = (↑n : ℝ) * arccos x) (hk' : (↑(↑k : ℤ) : ℝ) = (↑n : ℝ) * (arccos x / π)),
    ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
lift k to ℕ using (by rw [← Int.cast_nonneg_iff (R := ℝ), hk']; positivity [arccos_nonneg x])
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑(↑k : ℤ) : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑(↑k : ℤ) : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ (↑k : ℝ) * π = (↑n : ℝ) * arccos x

Tactic:
simp only [Int.cast_natCast] at hk hk'

Premises used: Int.cast_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑(↑k : ℤ) : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑(↑k : ℤ) : ℝ) = (↑n : ℝ) * (arccos x / π)
hk₁ : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
⊢ (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)

Tactic:
simp only [Int.cast_natCast] at hk hk'

Premises used: Int.cast_natCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
rw : (↑n : ℝ) * (arccos x / π) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) 1
⊢ LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
rw [← mul_one (n : ℝ), hk']

Premises used: Nat.cast, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hbc : arccos x / π ≤ 1
⊢ (↑n : ℝ) * (arccos x / π) ≤ HMul.hMul (α := ℝ) (↑n : ℝ) 1

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ 0 ≤ π

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ arccos x / π ≤ 1

Tactic:
exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)

Premises used: div_le_one_of_le₀, Real.arccos_le_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
⊢ LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)

Tactic:
have hkn : (k : ℝ) ≤ n := by
      rw [← mul_one (n : ℝ), hk']
      gcongr
      exact div_le_one_of_le₀ (arccos_le_pi x) (by positivity)
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ k ≤ n

Tactic:
simpa using hkn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
mp : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
refine ⟨k, by simpa using hkn, ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ cos ((↑n : ℝ) * arccos x / (↑n : ℝ)) = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
congr(cos ($hk.symm / n))

Premises used: Real.cos, congrArg, id, HDiv.hDiv, Nat.cast, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
h : x = cos ((↑n : ℝ) * arccos x / (↑n : ℝ))
⊢ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
convert! congr(cos ($hk.symm / n))
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ -1 ≤ x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
⊢ x ≤ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : (↑k : ℝ) * π = (↑n : ℝ) * arccos x
hk' : (↑k : ℝ) = (↑n : ℝ) * (arccos x / π)
hkn : LE.le (α := ℝ) (↑k : ℝ) (↑n : ℝ)
h : x = cos (arccos x)
h₁ h₂ : x = x
⊢ x = cos ((↑n : ℝ) * arccos x / (↑n : ℝ))

Tactic:
rw [mul_div_cancel_left₀ _ (by simpa), cos_arccos (by grind) (by grind)]

Premises used: mul_div_cancel_left₀, Real.cos_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
mpr : ∃ (k_1 : ℤ), (↑k_1 : ℝ) * π = (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))
⊢ |eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ))| = 1

Tactic:
rw [T_real_cos, abs_cos_eq_one_iff]

Premises used: Polynomial.Chebyshev.T_real_cos, Real.abs_cos_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ (↑(↑k : ℤ) : ℝ) * π = (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ≤ n
⊢ ∃ (k_1 : ℤ), (↑k_1 : ℝ) * π = (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
exact ⟨k, by simp [field]⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k n : ℕ
hn : n ≠ 0
rw : cos ((↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (β := ℤ) (-1) (↑k : ℤ)
⊢ eval (cos ((↑k : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) = (↑(↑(Int.negOnePow (↑k : ℤ)) : ℤ) : ℝ)

Tactic:
rw [T_real_cos, Int.cast_negOnePow]

Premises used: Polynomial.Chebyshev.T_real_cos, Int.cast_negOnePow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k n : ℕ
hn : n ≠ 0
⊢ cos ((↑(↑k : ℤ) : ℝ) * π) = HPow.hPow (α := ℝ) (β := ℤ) (-1) (↑k : ℤ)

Tactic:
Real.cos_int_mul_pi k

Premises used: Nat.cast, Real.cos_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k n : ℕ
hn : n ≠ 0
h : (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ)) = (↑(↑k : ℤ) : ℝ) * π
⊢ cos ((↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (β := ℤ) (-1) (↑k : ℤ)

Tactic:
convert! Real.cos_int_mul_pi k using 2

Premises used: Nat.cast, Real.cos_int_mul_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
k n : ℕ
hn : n ≠ 0
⊢ (↑(↑n : ℤ) : ℝ) * ((↑k : ℝ) * π / (↑n : ℝ)) = (↑(↑k : ℤ) : ℝ) * π

Tactic:
simp [field]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
mp : eval x (T ℝ (↑n : ℤ)) = 1 → ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : (∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → eval x (T ℝ (↑n : ℤ)) = 1
⊢ eval x (T ℝ (↑n : ℤ)) = 1 ↔ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
mp :
  ∀ (k : ℕ) (hk₁ : k ≤ n) (hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))), ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans abs_one)

Premises used: Iff.mpr, Iff.mp, Or.inl, abs_one, abs_eq_abs, Eq.trans, Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
h : k ≤ n ∧ Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
use k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ k ≤ n ∧ Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
⟨hk₁, ?_, hk₂⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
h : Even k
⊢ k ≤ n ∧ Even k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
refine ⟨hk₁, ?_, hk₂⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) (-1) k = 1

Tactic:
rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx

Premises used: Int.cast_negOnePow_natCast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
hx₁ : HPow.hPow (α := ℝ) (-1) k = 1
⊢ k ≤ n

Tactic:
rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx

Premises used: Int.cast_negOnePow_natCast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
hx₁ : HPow.hPow (α := ℝ) (-1) k = 1
hk₃ : k ≤ n
⊢ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx

Premises used: Int.cast_negOnePow_natCast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : HPow.hPow (α := ℝ) (-1) k = 1
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Ne (α := ℝ) (-1) 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : HPow.hPow (α := ℝ) (-1) k = 1
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Even k

Tactic:
exact (neg_one_pow_eq_one_iff_even (by grind)).mp hx

Premises used: neg_one_pow_eq_one_iff_even, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : Eq (α := ℝ) (↑(↑1 : ℤ) : ℝ) 1
⊢ eval x (T ℝ (↑n : ℤ)) = 1

Tactic:
rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_even k ((Int.even_coe_nat k).mpr hk₂)]

Premises used: Iff.mpr, Nat.cast, Int.negOnePow_even, Int.even_coe_nat, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Even k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr mpr₁ mpr₂ mpr₃ : Eq (α := ℤ) 1 1
⊢ Eq (α := ℝ) (↑(↑1 : ℤ) : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
mp : eval x (T ℝ (↑n : ℤ)) = -1 → ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : (∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → eval x (T ℝ (↑n : ℤ)) = -1
⊢ eval x (T ℝ (↑n : ℤ)) = -1 ↔ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
mp :
  ∀ (k : ℕ) (hk₁ : k ≤ n) (hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))), ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans ((abs_neg 1).trans abs_one))

Premises used: Iff.mpr, abs_neg, Iff.mp, Or.inl, abs_one, OfNat.ofNat, abs_eq_abs, Eq.trans, Polynomial.Chebyshev.abs_eval_T_real_eq_one_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
h : k ≤ n ∧ Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ ∃ k ≤ n, Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
use k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ k ≤ n ∧ Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
⟨hk₁, ?_, hk₂⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
h : Odd k
⊢ k ≤ n ∧ Odd k ∧ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
refine ⟨hk₁, ?_, hk₂⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ HPow.hPow (α := ℝ) (-1) k = -1

Tactic:
rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx

Premises used: Int.cast_negOnePow_natCast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
hx₁ : HPow.hPow (α := ℝ) (-1) k = -1
⊢ k ≤ n

Tactic:
rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx

Premises used: Int.cast_negOnePow_natCast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ (↑n : ℤ)) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
hx₁ : HPow.hPow (α := ℝ) (-1) k = -1
hk₃ : k ≤ n
⊢ x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx

Premises used: Int.cast_negOnePow_natCast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : HPow.hPow (α := ℝ) (-1) k = -1
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Ne (α := ℝ) (-1) 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : HPow.hPow (α := ℝ) (-1) k = -1
hk₁ : k ≤ n
hk₂ : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
⊢ Odd k

Tactic:
exact (neg_one_pow_eq_neg_one_iff_odd (by grind)).mp hx

Premises used: neg_one_pow_eq_neg_one_iff_odd, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : Eq (α := ℝ) (↑(↑(-1) : ℤ) : ℝ) (-1)
⊢ eval x (T ℝ (↑n : ℤ)) = -1

Tactic:
rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_odd k ((Int.odd_coe_nat k).mpr hk₂)]

Premises used: Iff.mpr, Int.odd_coe_nat, Int.negOnePow_odd, Nat.cast, Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hk₁ : k ≤ n
hk₂ : Odd k
hx : x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr mpr₁ mpr₂ mpr₃ : -1 = Int.negSucc 0
⊢ Eq (α := ℝ) (↑(↑(-1) : ℤ) : ℝ) (-1)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
inr :
  ∀
    (this :
      ∀ (n : ℕ) (hn : n ≠ 0),
        Multiset.Nodup (α := ℝ)
          (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
            (Multiset.range n)))
    (hn : n = 0),
    Multiset.Nodup (α := ℝ)
      (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Multiset.range n))
wlog! :
  ∀ (n : ℕ) (hn : n ≠ 0),
    Multiset.Nodup (α := ℝ)
      (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Multiset.range n))
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))

Tactic:
wlog! hn : n ≠ 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
this :
  ∀ (n : ℕ) (hn : n ≠ 0),
    Multiset.Nodup (α := ℝ)
      (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
        (Multiset.range n))
hn : n = 0
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))

Tactic:
(Finset.range n).nodup_map_iff_injOn.mpr ?_

Premises used: Iff.mpr, Multiset.ofList, Multiset.range, Finset.nodup_map_iff_injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
refine :
  Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (↑(Finset.range n) : Set ℕ)
⊢ Multiset.Nodup (α := ℝ)
    (Multiset.map (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
      (Multiset.range n))

Tactic:
refine (Finset.range n).nodup_map_iff_injOn.mpr ?_

Premises used: Iff.mpr, Finset.nodup_map_iff_injOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ))
    (↑(Finset.range n) : Set ℕ)

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ 0 ≤ (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
refine :
  ∀ (k : ℕ) (hk : k ∈ (↑(Finset.range n) : Set ℕ)),
    (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ) ≤ π
⊢ Set.InjOn (β := ℝ) (fun (k : ℕ) ↦ cos ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * π / HMul.hMul (α := ℝ) 2 (↑n : ℝ)))
    (↑(Finset.range n) : Set ℕ)

Tactic:
refine injOn_cos.comp (by aesop) fun k hk => Set.mem_Icc.mpr ⟨by positivity, ?_⟩

Premises used: Iff.mpr, Set.InjOn.comp, And.intro, Set.mem_Icc, Real.injOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
field_simp : 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 : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
norm_cast : 2 * k + 1 ≤ 2 * n
⊢ HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
k : ℕ
hk : k ∈ (↑(Finset.range n) : Set ℕ)
⊢ 2 * k + 1 ≤ 2 * n

Tactic:
grind