awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
rw : node n a < node n 0
⊢ node n a < 1

Tactic:
rw [← node_eq_one (n := n)]

Premises used: Polynomial.Chebyshev.node_eq_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ a ≤ n

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ 0 < a

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ node n a < node n 0

Tactic:
exact node_lt (by grind) (by grind)

Premises used: Polynomial.Chebyshev.node_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
s : Finset ℕ
hs : s ⊆ (Finset.range (n + 1)).erase i
hscard : s.card = n - k
hsn : 0 ∉ s
a : ℕ
ha : a ∈ s
⊢ 0 < x - node n a

Tactic:
grind [show node n a < 1 by rw [← node_eq_one (n := n)]; exact node_lt (by grind) (by grind)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
pos :
  ∀ (hk : n < k),
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
neg :
  ∀ (hk : k ≤ n),
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))

Tactic:
by_cases! hk : n < k
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
grw : LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑k : WithBot ℕ)
⊢ P.degree < (↑k : WithBot ℕ)

Tactic:
grw [hPdeg]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
⊢ LT.lt (α := WithBot ℕ) (↑n : WithBot ℕ) (↑k : WithBot ℕ)

Tactic:
simpa
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
⊢ degree (T ℝ (↑n : ℤ)) < (↑k : WithBot ℕ)

Tactic:
simp [hk]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : n < k
pos : eval x 0 ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
pos₁ pos₂ : eval x 0 ≤ eval x 0
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))

Tactic:
rw [iterate_derivative_eq_zero_of_degree_lt (by grw [hPdeg]; simpa),
      iterate_derivative_eq_zero_of_degree_lt (by simp [hk])]

Premises used: Polynomial.iterate_derivative_eq_zero_of_degree_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : k ≤ n
⊢ sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P ≤
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))

Tactic:
sumNodes_le_sumNodes_T (fun i hi => negOnePow_mul_iterateDerivativeC_nonneg hi hx) hPbnd

Premises used: Polynomial.Chebyshev.sumNodes_le_sumNodes_T, _private.0.Polynomial.Chebyshev.negOnePow_mul_iterateDerivativeC_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : k ≤ n
h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
h₁ :
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))
neg : ℕ
neg₁ : (i : ℕ) → ℕ
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))

Tactic:
convert!
    sumNodes_le_sumNodes_T (fun i hi => negOnePow_mul_iterateDerivativeC_nonneg hi hx) hPbnd using 1

Premises used: Polynomial.Chebyshev.sumNodes_le_sumNodes_T, _private.0.Polynomial.Chebyshev.negOnePow_mul_iterateDerivativeC_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : k ≤ n
h h₁ : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P

Tactic:
rw [sumNodes_eq_eval_iterate_derivative hk x hPdeg]

Premises used: _private.0.Polynomial.Chebyshev.sumNodes_eq_eval_iterate_derivative
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
hk : k ≤ n
h h₁ :
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))

Tactic:
rw [sumNodes_eq_eval_iterate_derivative hk x (le_of_eq (degree_T ℝ n))]

Premises used: Real, Polynomial.Chebyshev.degree_T, Nat.cast, le_of_eq, _private.0.Polynomial.Chebyshev.sumNodes_eq_eval_iterate_derivative
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
⊢ sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P =
      sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ)) ↔
    P = T ℝ (↑n : ℤ)

Tactic:
sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_iterateDerivativeC_pos hk₁ hk₂ hi hx)
      hPdeg hPbnd

Premises used: Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff, _private.0.Polynomial.Chebyshev.negOnePow_mul_iterateDerivativeC_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
h₁ :
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) ↔
    P = T ℝ (↑n : ℤ)

Tactic:
convert!
    sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_iterateDerivativeC_pos hk₁ hk₂ hi hx)
      hPdeg hPbnd using 2

Premises used: Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff, _private.0.Polynomial.Chebyshev.negOnePow_mul_iterateDerivativeC_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h h₁ : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P

Tactic:
rw [sumNodes_eq_eval_iterate_derivative hk₂ x hPdeg]

Premises used: _private.0.Polynomial.Chebyshev.sumNodes_eq_eval_iterate_derivative
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
P : ℝ[X]
k : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
x : ℝ
hx : 1 ≤ x
hPdeg : P.degree ≤ (↑n : WithBot ℕ)
hPbnd : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) x → |eval x P| ≤ 1
h h₁ :
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))

Tactic:
rw [sumNodes_eq_eval_iterate_derivative hk₂ x (le_of_eq (degree_T ℝ n))]

Premises used: Real, Polynomial.Chebyshev.degree_T, Nat.cast, le_of_eq, _private.0.Polynomial.Chebyshev.sumNodes_eq_eval_iterate_derivative
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
x : ℝ
⊢ 0 ≤ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ LE.le (α := ℝ) (-1) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ MeasurableSet (α := ℝ) (Set.Ioc (-1) 1)

Tactic:
measurability
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ Measurable (β := ℝ≥0) fun (x : ℝ) ↦ NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Set.Ioc (-1) 1)) fun (x : ℝ) ↦
      NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯ • f x)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Set.Ioc (-1) 1)) fun (x : ℝ) ↦
      f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
⊢ Eq (α := ℝ) (∫ (x : ℝ), f x ∂measureT) (∫ (x : ℝ) in -1..1, f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
rw [integral_of_le (by norm_num), measureT,
    restrict_withDensity (by measurability),
    integral_withDensity_eq_integral_smul (by fun_prop)]

Premises used: Polynomial.Chebyshev.measureT, integral_withDensity_eq_integral_smul, MeasureTheory.restrict_withDensity, intervalIntegral.integral_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
h : ∀ (x : ℝ), NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯ • f x = f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Set.Ioc (-1) 1)) fun (x : ℝ) ↦
      NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯ • f x)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Set.Ioc (-1) 1)) fun (x : ℝ) ↦
      f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
congr! 2 with x hx
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
x : ℝ
⊢ NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯ • f x = f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
simp [NNReal.smul_def, mul_comm]

Premises used: NNReal.smul_def, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
rw :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.uIoc (-1) 1) volume
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) volume (-1) 1

Tactic:
rw [intervalIntegrable_iff]

Premises used: intervalIntegrable_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (min (-1) 1) (max (-1) 1)) x → 0 ≤ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
refine :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioo (min (-1) 1) (max (-1) 1)) x),
    HasDerivAt (fun (x : ℝ) ↦ -arccos x) (√(1 - HPow.hPow (β := ℕ) x 2)⁻¹) x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.uIoc (-1) 1) volume

Tactic:
refine integrableOn_deriv_of_nonneg continuous_arccos.neg.continuousOn (fun x hx ↦ ?_) (by simp)

Premises used: Continuous.neg, intervalIntegral.integrableOn_deriv_of_nonneg, Continuous.continuousOn, Real.continuous_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (min (-1) 1) (max (-1) 1)) x
⊢ x ≠ -1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (min (-1) 1) (max (-1) 1)) x
⊢ x ≠ 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioo (min (-1) 1) (max (-1) 1)) x
⊢ HasDerivAt (fun (x : ℝ) ↦ -arccos x) (√(1 - HPow.hPow (β := ℕ) x 2)⁻¹) x

Tactic:
simpa using (hasDerivAt_arccos (by aesop) (by aesop)).neg

Premises used: Real.hasDerivAt_arccos, HasDerivAt.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ LT.lt (α := ℝ) (-1) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
rwa rwa₁ rwa₂ rwa₃ : ContinuousOn f (Set.Icc (-1) 1)
⊢ ContinuousOn f (Set.uIcc (-1) 1)

Tactic:
rwa [Set.uIcc_of_lt (by norm_num)]

Premises used: Set.uIcc_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ ContinuousOn f (Set.uIcc (-1) 1)

Tactic:
replace hf : ContinuousOn f (Set.uIcc (-1) 1) := by rwa [Set.uIcc_of_lt (by norm_num)]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) volume (-1) 1

Tactic:
have := intervalIntegrable_sqrt_one_sub_sq_inv.continuousOn_mul hf
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.uIoc (-1) 1)
    volume
⊢ LE.le (α := ℝ) (-1) 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) volume (-1) 1
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.Ioc (-1) 1)
    volume

Tactic:
rw [intervalIntegrable_iff, Set.uIoc_of_le (by norm_num)] at this

Premises used: intervalIntegrable_iff, Set.uIoc_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.Ioc (-1) 1)
    volume
⊢ MeasurableSet (α := ℝ) (Set.Ioc (-1) 1)

Tactic:
measurability
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.Ioc (-1) 1)
    volume
⊢ Measurable (β := ENNReal) fun (x : ℝ) ↦ (↑(NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯) : ENNReal)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.Ioc (-1) 1)
    volume
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioc (-1) 1), (↑(NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯) : ENNReal) < ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.Ioc (-1) 1)
    volume
rw :
  @Integrable ℝ _ _ _ measurableSpace
    (fun (x : ℝ) ↦ f x * (↑(NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯) : ENNReal).toReal)
    (Measure.restrict volume (Set.Ioc (-1) 1))
⊢ Integrable f measureT

Tactic:
rw [measureT, restrict_withDensity (by measurability),
    integrable_withDensity_iff (by fun_prop) (by simp)]

Premises used: Polynomial.Chebyshev.measureT, MeasureTheory.restrict_withDensity, MeasureTheory.integrable_withDensity_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (Measure.restrict volume (Set.Ioc (-1) 1))
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (Measure.restrict volume (Set.Ioc (-1) 1))

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this :
  @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (Measure.restrict volume (Set.Ioc (-1) 1))
⊢ @Integrable ℝ _ _ _ measurableSpace
    (fun (x : ℝ) ↦ f x * (↑(NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ ⋯) : ENNReal).toReal)
    (Measure.restrict volume (Set.Ioc (-1) 1))

Tactic:
convert! this
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, -(f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹))
    (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in -1..1, f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
rw [integral_symm, ← intervalIntegral.integral_neg]

Premises used: intervalIntegral.integral_symm, intervalIntegral.integral_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, -(f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹))
    (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
rw :
  Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (x : ℝ) in 1..-1, ((fun (θ : ℝ) ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - HPow.hPow (β := ℕ) x 2)))
hf : ContinuousOn arccos (uIcc 1 (-1))
hff' :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x →
      HasDerivAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) x
hf' :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x → -(1 / √(1 - HPow.hPow (β := ℕ) x 2)) ≤ 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ))

Tactic:
rw [← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))]

Premises used: intervalIntegral.integral_comp_mul_deriv_of_deriv_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
simp_rw :
  Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (x : ℝ) in 1..-1, f (cos (arccos x)) * -(1 / √(1 - HPow.hPow (β := ℕ) x 2)))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (x : ℝ) in 1..-1, ((fun (θ : ℝ) ↦ f (cos θ)) ∘ arccos) x * -(1 / √(1 - HPow.hPow (β := ℕ) x 2)))

Tactic:
simp_rw [Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (uIcc 1 (-1)) x
⊢ -1 ≤ x

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (uIcc 1 (-1)) x
⊢ x ≤ 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (uIcc 1 (-1)) x
⊢ f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹ = f (cos (arccos x)) * -(1 / √(1 - HPow.hPow (β := ℕ) x 2))

Tactic:
simp [cos_arccos (x := x) (by aesop) (by aesop)]

Premises used: Real.cos_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (x : ℝ) in 1..-1, f (cos (arccos x)) * -(1 / √(1 - HPow.hPow (β := ℕ) x 2)))

Tactic:
exact integral_congr <| fun x hx => by simp [cos_arccos (x := x) (by aesop) (by aesop)]

Premises used: intervalIntegral.integral_congr
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ ContinuousOn arccos (uIcc 1 (-1))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x
⊢ x ≠ -1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x
⊢ x ≠ 1

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x →
      HasDerivAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) x

Tactic:
exact fun x hx ↦ (hasDerivAt_arccos (by aesop) (by aesop))

Premises used: Real.hasDerivAt_arccos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x → -(1 / √(1 - HPow.hPow (β := ℕ) x 2)) ≤ 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
f : ℝ → ℝ
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ)) (∫ (θ : ℝ) in 0..π, f (cos θ))

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

Tactic:
rw [integral_measureT_eq_integral_cos]

Premises used: Polynomial.Chebyshev.integral_measureT_eq_integral_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality
Goal:
⊢ ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ 0) = π

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

Tactic:
have hn' : (n : ℝ) ≠ 0 := Int.cast_ne_zero.mpr hn