awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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 : ℕ
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) ≤ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
have neg₁ : (i : ℕ) → ℕ
Tactic: convert!
    sumNodes_le_sumNodes_T (fun i hi => negOnePow_mul_iterateDerivativeC_nonneg hi hx) hPbnd using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
have h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)
Tactic: rw [sumNodes_eq_eval_iterate_derivative hk x hPdeg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))
have h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: rw [sumNodes_eq_eval_iterate_derivative hk x (le_of_eq (degree_T ℝ n))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) ↔
    P = T ℝ (↑n : ℤ)
have h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
Tactic: convert!
    sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_iterateDerivativeC_pos hk₁ hk₂ hi hx)
      hPdeg hPbnd using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) ↔
    P = T ℝ (↑n : ℤ)
have h₁ : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
  sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))
Tactic: convert!
    sumNodes_eq_sumNodes_T_iff (fun i hi => negOnePow_mul_iterateDerivativeC_pos hk₁ hk₂ hi hx)
      hPdeg hPbnd using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) P
have h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P) = eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] P)
Tactic: rw [sumNodes_eq_eval_iterate_derivative hk₂ x hPdeg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
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
⊢ eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
    sumNodes n (fun (i : ℕ) ↦ iterateDerivativeC n k x i) (T ℝ (↑n : ℤ))
have h : eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ))) =
  eval x ((⇑derivative : (a : ℝ[X]) → ℝ[X])^[k] (T ℝ (↑n : ℤ)))
Tactic: rw [sumNodes_eq_eval_iterate_derivative hk₂ x (le_of_eq (degree_T ℝ n))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
f : ℝ → ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ), f x ∂measureT) (∫ (x : ℝ) in -1..1, f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Set.Ioc (-1) 1)) fun (x : ℝ) ↦
    NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ sorry • f x)
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Set.Ioc (-1) 1)) fun (x : ℝ) ↦
    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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
f : ℝ → ℝ
⊢ 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)⁻¹)
have h : ∀ (x : ℝ), NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ sorry • f x = f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: congr! 2 with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) volume (-1) 1
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.uIoc (-1) 1) volume
Tactic: rw [intervalIntegrable_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) (Set.uIoc (-1) 1) volume
have 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
Tactic: refine integrableOn_deriv_of_nonneg continuous_arccos.neg.continuousOn (fun x hx ↦ ?_) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (hypothesis)
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ Integrable f measureT
have hf₁ : ContinuousOn f (Set.uIcc (-1) 1)
Tactic: replace hf : ContinuousOn f (Set.uIcc (-1) 1) := by rwa [Set.uIcc_of_lt (by norm_num)]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (hypothesis)
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
⊢ Integrable f measureT
have this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) volume (-1) 1
Tactic: have := intervalIntegrable_sqrt_one_sub_sq_inv.continuousOn_mul hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (hypothesis)
Goal:
f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ f x * √(1 - HPow.hPow (β := ℕ) x 2)⁻¹) volume (-1) 1
⊢ Integrable f measureT
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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
⊢ Integrable f measureT
have rw : @Integrable ℝ _ _ _ measurableSpace
  (fun (x : ℝ) ↦ f x * (↑(NNReal.mk √(1 - HPow.hPow (β := ℕ) x 2)⁻¹ sorry) : ENNReal).toReal)
  (Measure.restrict volume (Set.Ioc (-1) 1))
Tactic: rw [measureT, restrict_withDensity (by measurability),
    integrable_withDensity_iff (by fun_prop) (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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)⁻¹)
have rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
f : ℝ → ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ))
have 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)))
Tactic: rw [← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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)))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ))
have hf : ContinuousOn arccos (uIcc 1 (-1))
Tactic: rw [← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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))
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ))
have hff' : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x →
    HasDerivAt arccos (-(1 / √(1 - HPow.hPow (β := ℕ) x 2))) x
Tactic: rw [← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 1..-1, f x * -√(1 - HPow.hPow (β := ℕ) x 2)⁻¹)
    (∫ (θ : ℝ) in arccos 1..arccos (-1), f (cos θ))
have hf' : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioo (min 1 (-1)) (max 1 (-1))) x → -(1 / √(1 - HPow.hPow (β := ℕ) x 2)) ≤ 0
Tactic: rw [← integral_comp_mul_deriv_of_deriv_nonpos (f' := fun x => -(1 / √(1 - x ^ 2)))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
f : ℝ → ℝ
⊢ 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)))
have 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)))
Tactic: simp_rw [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
⊢ ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π
have rw : ∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ 0) = π
Tactic: rw [integral_measureT_eq_integral_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (hypothesis)
Goal:
n : ℤ
hn : n ≠ 0
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ n) ∂measureT) 0
have hn' : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: have hn' : (n : ℝ) ≠ 0 := Int.cast_ne_zero.mpr hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ n) ∂measureT) 0
have rw : Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ n)) 0
Tactic: rw [integral_measureT_eq_integral_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, eval (cos θ) (T ℝ n)) 0
have simp_rw : Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, cos ((↑n : ℝ) * θ)) 0
Tactic: simp_rw [T_real_cos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
this : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, cos ((↑n : ℝ) * θ)) 0
have rwa : HSMul.hSMul (α := ℝ) (β := ℝ) (↑n : ℝ)⁻¹ (∫ (x : ℝ) in HMul.hMul (α := ℝ) (↑n : ℝ) 0..(↑n : ℝ) * π, cos x) = 0
Tactic: rwa [integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn), smul_eq_zero_iff_right (by aesop),
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..π, cos ((↑n : ℝ) * θ)) 0
have rwa₁ : Eq (α := ℝ) (∫ (x : ℝ) in HMul.hMul (α := ℝ) (↑n : ℝ) 0..(↑n : ℝ) * π, cos x) 0
Tactic: rwa [integral_comp_mul_left _ (Int.cast_ne_zero.mpr hn), smul_eq_zero_iff_right (by aesop),
      mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ n) ∂measureT) 0
have suffices : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
have trans : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ)
Tactic: trans ∫ θ in 0..n * π, (deriv sin) θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
trans : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ)
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, cos θ) 0
have trans₁ : Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
Tactic: trans ∫ θ in 0..n * π, (deriv sin) θ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
have by_cases! : 0 ≤ n → Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
Tactic: by_cases! 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
by_cases! : 0 ≤ n → Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
have neg : n < 0 → Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
Tactic: by_cases! 0 ≤ n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
h : 0 ≤ n
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
have rw : sin ((↑n : ℝ) * π) - sin 0 = 0
Tactic: rw [integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn_1 : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
hn : n < 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
have rw : -(sin 0 - sin ((↑n : ℝ) * π)) = 0
Tactic: rw [integral_symm, integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℤ
hn_1 : n ≠ 0
hn' : Ne (α := ℝ) (↑n : ℝ) 0
hn : n < 0
rw : -(sin 0 - sin ((↑n : ℝ) * π)) = 0
⊢ Eq (α := ℝ) (∫ (θ : ℝ) in 0..(↑n : ℝ) * π, deriv sin θ) 0
have rw₁ : (↑n : ℝ) * π ≤ 0
Tactic: rw [integral_symm, integral_deriv_of_contDiffOn_Icc contDiff_sin.contDiffOn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (hypothesis)
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 : ℝ), 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
have 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)
Tactic: simp_rw [eval_mul, eval_ofNat, mul_assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (hypothesis)
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)
⊢ ∫ (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
have 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)
Tactic: rw [MeasureTheory.integral_const_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n m : ℤ
⊢ ∫ (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
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n m : ℤ
⊢ ∫ (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)
have 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)
Tactic: simp_rw [T_mul_T, eval_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n m : ℤ
⊢ ∫ (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)
have 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)
Tactic: rw [MeasureTheory.integral_add
    (integrable_measureT (by fun_prop)) (integrable_measureT (by fun_prop))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n m : ℕ
h : n ≠ m
⊢ Eq (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑m : ℤ)) ∂measureT) 0
have rw : HAdd.hAdd (α := ℝ) 0 0 / 2 = 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)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
⊢ ∫ (x : ℝ), eval x (T ℝ 0) * eval x (T ℝ 0) ∂measureT = π
have simp_rw : ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = π
Tactic: simp_rw [← eval_mul, show (T ℝ 0) * (T ℝ 0) = T ℝ 0 by simp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ ∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑n : ℤ)) ∂measureT = π / 2
have rw : HAdd.hAdd (α := ℝ) (∫ (x : ℝ), eval x (T ℝ (HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT)
      (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) /
    2 =
  π / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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
⊢ ∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑n : ℤ)) ∂measureT = π / 2
have rw₁ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ (HSub.hSub (α := ℤ) (↑n : ℤ) (↑n : ℤ))) ∂measureT) / 2 = π / 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality (goal)
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
⊢ ∫ (x : ℝ), eval x (T ℝ (↑n : ℤ)) * eval x (T ℝ (↑n : ℤ)) ∂measureT = π / 2
have rw₂ : HAdd.hAdd (α := ℝ) 0 (∫ (x : ℝ), eval x (T ℝ 0) ∂measureT) / 2 = π / 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]