awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
rw : Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ n)) 0
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ n) ∂measureT) 0

Tactic:
rw [integral_measureT_eq_integral_cos]

Premises used: Polynomial.Chebyshev.integral_measureT_eq_integral_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
simp_rw : Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, cos ((↑n : ℝ) * θ)) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ n)) 0

Tactic:
simp_rw [T_real_cos]

Premises used: Polynomial.Chebyshev.T_real_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
⊢ Ne (α := ℝ) (↑n : ℝ)⁻¹ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
rwa : HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∫ (x : ℝ) in HMul.hMul (α := ℝ) (↑n : ℝ) 0..(↑n : ℝ) * π, cos x) = 0
rwa₁ : Eq (α := ℝ) (∫ (x : ℝ) in HMul.hMul (α := ℝ) (↑n : ℝ) 0..(↑n : ℝ) * π, cos x) 0
rwa₂ rwa₃ rwa₄ rwa₅ : Eq (α := ℝ) (∫ (x : ℝ) in 0..(↑n : ℝ) * π, cos x) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, cos ((↑n : ℝ) * θ)) 0

Tactic:
rwa [integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn), smul_eq_zero_iff_right (by aesop),
      mul_zero]

Premises used: Iff.mpr, intervalIntegral.integral_comp_mul_left, MulZeroClass.mul_zero, smul_eq_zero_iff_right, Int.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
suffices : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ n) ∂measureT) 0

Tactic:
suffices ∫ θ in 0..n * π, cos θ = 0 by
    rw [integral_measureT_eq_integral_cos]
    simp_rw [T_real_cos]
    rwa [integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn), smul_eq_zero_iff_right (by aesop),
      mul_zero]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
trans : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ)
trans₁ : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0

Tactic:
trans ∫ θ in 0..n * π, (deriv sin) θ
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ)

Tactic:
integral_congr <| fun x hx => (congrFun deriv_sin x).symm

Premises used: intervalIntegral.integral_congr, congrFun, Eq.symm, Real.deriv_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ)

Tactic:
refine integral_congr <| fun x hx => (congrFun deriv_sin x).symm

Premises used: intervalIntegral.integral_congr, congrFun, Eq.symm, Real.deriv_sin
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
by_cases! : 0 ≤ n → Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
neg : n < 0 → Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0

Tactic:
by_cases! 0 ≤ n
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
h : 0 ≤ n
⊢ 0 ≤ (↑n : ℝ) * π

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
h : 0 ≤ n
rw : sin ((↑n : ℝ) * π) - sin 0 = 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0

Tactic:
rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]

Premises used: ContDiff.contDiffOn, Real.contDiff_sin, intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
h : 0 ≤ n
⊢ sin ((↑n : ℝ) * π) - sin 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
h : 0 ≤ n
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0

Tactic:
case pos => rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]; simp

Premises used: ContDiff.contDiffOn, Real.contDiff_sin, intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn_1 : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
hn : n < 0
rw : -(sin 0 - sin ((↑n : ℝ) * π)) = 0
rw₁ : (↑n : ℝ) * π ≤ 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0

Tactic:
rw [integral_symm, integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn]

Premises used: ContDiff.contDiffOn, Real.contDiff_sin, intervalIntegral.integral_symm, intervalIntegral.integral_deriv_of_contDiffOn_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn_1 : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
hn : n < 0
⊢ -(sin 0 - sin ((↑n : ℝ) * π)) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn_1 : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
hn : n < 0
⊢ (↑n : ℝ) * π ≤ 0

Tactic:
mul_nonpos_of_nonpos_of_nonneg (Int.cast_nonpos.mpr <| le_of_lt hn) pi_nonneg

Premises used: Iff.mpr, mul_nonpos_of_nonpos_of_nonneg, Real.pi_nonneg, le_of_lt, Int.cast_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℤ
hn_1 : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
hn : n < 0
⊢ (↑n : ℝ) * π ≤ 0

Tactic:
exact mul_nonpos_of_nonpos_of_nonneg (Int.cast_nonpos.mpr <| le_of_lt hn) pi_nonneg

Premises used: mul_nonpos_of_nonpos_of_nonneg, Real.pi_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
this :
  ∫ (x : ℝ), eval x (HMul.hMul (α := ℝ[X]) 2 (T ℝ n) * T ℝ m) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)
⊢ ∫ (x : ℝ), 2 * (eval x (T ℝ n) * eval x (T ℝ m)) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)

Tactic:
simp_rw [eval_mul, eval_ofNat, mul_assoc] at this

Premises used: mul_assoc, Polynomial.eval_mul, Polynomial.eval_ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
this :
  ∫ (x : ℝ), 2 * (eval x (T ℝ n) * eval x (T ℝ m)) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)
⊢ HMul.hMul (α := ℝ) 2 (∫ (a : ℝ), eval a (T ℝ n) * eval a (T ℝ m) ∂measureT) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)

Tactic:
rw [MeasureTheory.integral_const_mul] at this

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
this :
  HMul.hMul (α := ℝ) 2 (∫ (a : ℝ), eval a (T ℝ n) * eval a (T ℝ m) ∂measureT) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
suffices :
  ∫ (x : ℝ), eval x (HMul.hMul (α := ℝ[X]) 2 (T ℝ n) * T ℝ m) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)
⊢ ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

Tactic:
suffices ∫ x, (2 * T ℝ n * T ℝ m).eval x ∂measureT =
      (∫ x, (T ℝ (n + m)).eval x ∂measureT) +
      (∫ x, (T ℝ (n - m)).eval x ∂measureT) by
    simp_rw [eval_mul, eval_ofNat, mul_assoc] at this
    rw [MeasureTheory.integral_const_mul] at this
    grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
simp_rw :
  ∫ (x : ℝ), eval x (T ℝ (n + m)) + eval x (T ℝ (n - m)) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)
⊢ ∫ (x : ℝ), eval x (HMul.hMul (α := ℝ[X]) 2 (T ℝ n) * T ℝ m) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)

Tactic:
simp_rw [T_mul_T, eval_add]

Premises used: Polynomial.eval_add, Polynomial.Chebyshev.T_mul_T
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (n + m))) (Set.Icc (-1) 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ eval x (T ℝ (n - m))) (Set.Icc (-1) 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℤ
rw rw₁ :
  HAdd.hAdd (α := ℝ) (∫ (a : ℝ), eval a (T ℝ (n + m)) ∂measureT) (∫ (a : ℝ), eval a (T ℝ (n - m)) ∂measureT) =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)
⊢ ∫ (x : ℝ), eval x (T ℝ (n + m)) + eval x (T ℝ (n - m)) ∂measureT =
    HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT) (∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT)

Tactic:
rw [MeasureTheory.integral_add
    (integrable_measureT (by fun_prop)) (integrable_measureT (by fun_prop))]

Premises used: Polynomial.Chebyshev.integrable_measureT, MeasureTheory.integral_add
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℕ
h : n ≠ m
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑m : ℤ) ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℕ
h : n ≠ m
⊢ HSub.hSub (α := ℤ) (↑n : ℤ) (↑m : ℤ) ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℕ
h : n ≠ m
rw : HAdd.hAdd (α := ℝ) 0 0 / 2 = 0
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑m : ℤ)) ∂measureT) 0

Tactic:
rw [integral_eval_T_real_mul_eval_T_real_measureT,
    integral_eval_T_real_measureT_of_ne_zero (by grind),
    integral_eval_T_real_measureT_of_ne_zero (by grind)]

Premises used: Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT, Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n m : ℕ
h : n ≠ m
⊢ HAdd.hAdd (α := ℝ) 0 0 / 2 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
⊢ HMul.hMul (α := ℝ[X]) (T ℝ 0) (T ℝ 0) = T ℝ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
simp_rw : ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π
⊢ ∫ (x : ℝ), eval x (T ℝ 0) * eval x (T ℝ 0) ∂measureT = π

Tactic:
simp_rw [← eval_mul, show (T ℝ 0) * (T ℝ 0) = T ℝ 0 by simp]

Premises used: Polynomial.eval_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
⊢ ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π

Tactic:
integral_eval_T_real_measureT_zero

Premises used: Polynomial.Chebyshev.integral_eval_T_real_measureT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
⊢ ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π

Tactic:
exact integral_eval_T_real_measureT_zero

Premises used: Polynomial.Chebyshev.integral_eval_T_real_measureT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℕ
hn : n ≠ 0
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ) ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
n : ℕ
hn : n ≠ 0
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT)
        (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) /
      2 =
    π / 2
rw₁ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) / 2 = π / 2
rw₂ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ 0) ∂measureT) / 2 = π / 2
rw₃ : (0 + π) / 2 = π / 2
rw₄ rw₅ : π / 2 = π / 2
⊢ ∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑n : ℤ)) ∂measureT = π / 2

Tactic:
rw [integral_eval_T_real_mul_eval_T_real_measureT,
    integral_eval_T_real_measureT_of_ne_zero (by grind), sub_self,
    integral_eval_T_real_measureT_zero, zero_add]

Premises used: sub_self, Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, zero_add, Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT, Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ -1 ≤ x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ x ≤ 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
rw : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (eval (cos (arccos x)) (T ℝ n))
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (eval x (T ℝ n))

Tactic:
rw [← cos_arccos (x := x) (by grind) (by grind)]

Premises used: Real.cos_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (eval (cos (arccos x)) (T ℝ n))

Tactic:
grind [T_real_cos, cos_mem_Icc]

Premises used: Polynomial.Chebyshev.T_real_cos, Real.cos_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : |x| ≤ 1
⊢ |eval x (T ℝ n)| ≤ 1

Tactic:
grind [eval_T_real_mem_Icc]

Premises used: Polynomial.Chebyshev.eval_T_real_mem_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ x
rw : 1 ≤ eval (cosh (arcosh x)) (T ℝ n)
⊢ 1 ≤ eval x (T ℝ n)

Tactic:
rw [← cosh_arcosh hx]

Premises used: Real.cosh_arcosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ x
⊢ 1 ≤ eval (cosh (arcosh x)) (T ℝ n)

Tactic:
grind [T_real_cosh, one_le_cosh]

Premises used: Real.one_le_cosh, Polynomial.Chebyshev.T_real_cosh
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ arcosh x ≠ 0

Tactic:
grind [cosh_arcosh, cosh_zero]

Premises used: Real.cosh_arcosh, Real.cosh_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
⊢ arcosh x ≠ 0

Tactic:
have : arcosh x ≠ 0 := by grind [cosh_arcosh, cosh_zero]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
rw : Ne (α := ℝ) (↑n : ℝ) 0 ∧ arcosh x ≠ 0
⊢ 1 < eval x (T ℝ n)

Tactic:
rw [← cosh_arcosh (le_of_lt hx), T_real_cosh, one_lt_cosh, mul_ne_zero_iff]

Premises used: Real.cosh_arcosh, le_of_lt, Real.one_lt_cosh, Polynomial.Chebyshev.T_real_cosh, mul_ne_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬n = 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ arcosh x ≠ 0

Tactic:
assumption
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0 ∧ arcosh x ≠ 0

Tactic:
exact ⟨by norm_cast, by assumption⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
rw : 1 ≤ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))
⊢ 1 ≤ (↑(↑n.negOnePow : ℤ) : ℝ) * eval x (T ℝ n)

Tactic:
rw [← neg_neg x, T_eval_neg]

Premises used: Polynomial.Chebyshev.T_eval_neg, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ 1 ≤ eval (-x) (T ℝ n)

Tactic:
one_le_eval_T_real n (le_neg_of_le_neg hx)

Premises used: le_neg_of_le_neg, Polynomial.Chebyshev.one_le_eval_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
h : (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
⊢ 1 ≤ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))

Tactic:
convert! one_le_eval_T_real n (le_neg_of_le_neg hx)

Premises used: le_neg_of_le_neg, Polynomial.Chebyshev.one_le_eval_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
h : HMul.hMul (α := ℝ) (-1) (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
⊢ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)

Tactic:
rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]

Premises used: mul_assoc, Int.cast_negOnePow, mul_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : x ≤ -1
⊢ HMul.hMul (α := ℝ) (-1) (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
rw : 1 < (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))
⊢ 1 < (↑(↑n.negOnePow : ℤ) : ℝ) * eval x (T ℝ n)

Tactic:
rw [← neg_neg x, T_eval_neg]

Premises used: Polynomial.Chebyshev.T_eval_neg, neg_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ 1 < eval (-x) (T ℝ n)

Tactic:
one_lt_eval_T_real hn (lt_neg_of_lt_neg hx)

Premises used: Polynomial.Chebyshev.one_lt_eval_T_real, lt_neg_of_lt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
h : (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)
⊢ 1 < (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n))

Tactic:
convert! one_lt_eval_T_real hn (lt_neg_of_lt_neg hx)

Premises used: Polynomial.Chebyshev.one_lt_eval_T_real, lt_neg_of_lt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
h : HMul.hMul (α := ℝ) (-1) (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)
⊢ (↑(↑n.negOnePow : ℤ) : ℝ) * ((↑(↑n.negOnePow : ℤ) : ℝ) * eval (-x) (T ℝ n)) = eval (-x) (T ℝ n)

Tactic:
rw [Int.cast_negOnePow, ← mul_assoc, ← mul_zpow]

Premises used: mul_assoc, Int.cast_negOnePow, mul_zpow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : x < -1
⊢ HMul.hMul (α := ℝ) (-1) (-1) ^ n * eval (-x) (T ℝ n) = eval (-x) (T ℝ n)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
inr : ∀ (this : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|) (h : x < 0), 1 ≤ |eval x (T ℝ n)|
wlog! : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
wlog! h : 0 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
this : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|
h : x < 0
⊢ 1 ≤ |(-x)|

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
this : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|
h : x < 0
⊢ 0 ≤ -x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
this : ∀ (n : ℤ) {x : ℝ} (hx : 1 ≤ |x|) (h : 0 ≤ x), 1 ≤ |eval x (T ℝ n)|
h : x < 0
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
simpa [T_eval_neg, abs_mul, abs_unit_intCast] using @this n (-x) (by grind) (by grind)

Premises used: Polynomial.Chebyshev.T_eval_neg, abs_mul, abs_unit_intCast
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
h : 0 ≤ x
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
one_le_eval_T_real n (abs_of_nonneg h ▸ hx) |>.trans <| le_abs_self _

Premises used: le_abs_self, Polynomial.Chebyshev.one_le_eval_T_real, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
x : ℝ
hx : 1 ≤ |x|
h : 0 ≤ x
⊢ 1 ≤ |eval x (T ℝ n)|

Tactic:
exact one_le_eval_T_real n (abs_of_nonneg h ▸ hx) |>.trans <| le_abs_self _

Premises used: le_abs_self, Polynomial.Chebyshev.one_le_eval_T_real, LE.le.trans
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
inr :
  ∀ (this : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|) (h : x < 0),
    1 < |eval x (T ℝ n)|
wlog! : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|
⊢ 1 < |eval x (T ℝ n)|

Tactic:
wlog! h : 0 ≤ x
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
this : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|
h : x < 0
⊢ 1 < |(-x)|

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
this : ∀ {n : ℤ} (hn : n ≠ 0) {x : ℝ} (hx : 1 < |x|) (h : 0 ≤ x), 1 < |eval x (T ℝ n)|
h : x < 0
⊢ 0 ≤ -x

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
h : 0 ≤ x
⊢ 1 < |eval x (T ℝ n)|

Tactic:
one_lt_eval_T_real hn (abs_of_nonneg h ▸ hx) |>.trans_le <| le_abs_self _

Premises used: le_abs_self, LT.lt.trans_le, Polynomial.Chebyshev.one_lt_eval_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
h : 0 ≤ x
⊢ 1 < |eval x (T ℝ n)|

Tactic:
exact one_lt_eval_T_real hn (abs_of_nonneg h ▸ hx) |>.trans_le <| le_abs_self _

Premises used: le_abs_self, LT.lt.trans_le, Polynomial.Chebyshev.one_lt_eval_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℤ
hn : n ≠ 0
x : ℝ
⊢ |eval x (T ℝ n)| ≤ 1 → |x| ≤ 1

Tactic:
simpa using mt <| one_lt_abs_eval_T_real hn

Premises used: mt, Polynomial.Chebyshev.one_lt_abs_eval_T_real
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
mp : |eval x (T ℝ (↑n : ℤ))| = 1 → ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))
mpr : (∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))) → |eval x (T ℝ (↑n : ℤ))| = 1
⊢ |eval x (T ℝ (↑n : ℤ))| = 1 ↔ ∃ k ≤ n, x = cos ((↑k : ℝ) * π / (↑n : ℝ))

Tactic:
constructor