awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this : HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
⊢ Eq (α := ℂ)
    (∑ x ∈ range n,
      (Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) +
        Complex.exp
          ((↑(-k) : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑x : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)))
    0
have inr : Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I) /
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) +
    (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ /
      ((Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ - 1) =
  0
Tactic: rw [sum_add_distrib, sum_exp hn hk, sum_exp hn (by aesop),
    Int.cast_neg, neg_div, neg_mul, neg_mul, Complex.exp_neg,
    neg_div, neg_mul, neg_mul, Complex.exp_neg, this, ← add_mul, mul_eq_zero_of_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this : HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
⊢ Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I) /
        (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) +
      (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ /
        ((Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ - 1) =
    0
have inr : let z := Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I);
∀ (hz : z = Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)),
  z / (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) +
      z⁻¹ / ((Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ - 1) =
    0
Tactic: set z := exp (k / (2 * n) * π * I) with hz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this : HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
z : ℂ := Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)
hz : z = Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)
⊢ Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = HPow.hPow (β := ℕ) z 2
have rw : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) =
  Complex.exp ((↑2 : ℂ) * ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))
Tactic: rw [hz, ← Complex.exp_nat_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this : HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
z : ℂ := Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)
hz : z = Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)
⊢ z / (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) +
      z⁻¹ / ((Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ - 1) =
    0
have hz₂ : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = HPow.hPow (β := ℕ) z 2
Tactic: have hz₂ : exp (k / n * π * I) = z ^ 2 := by rw [hz, ← Complex.exp_nat_mul]; grind
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this : HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
z : ℂ := Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)
hz : z = Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)
hz₂ : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = HPow.hPow (β := ℕ) z 2
⊢ z / (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) +
      z⁻¹ / ((Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ - 1) =
    0
have inr : z / (HPow.hPow (β := ℕ) z 2 - 1) + z⁻¹ / (HPow.hPow (β := ℕ) z⁻¹ 2 - 1) = 0
Tactic: rw [hz₂, ← inv_pow z 2]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule ℝ ℝ[X]) (degreeLT ℝ (2 * n)) P
have rwa : P.degree < (↑(2 * n) : WithBot ℕ)
Tactic: rwa [mem_degreeLT]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
have hmem : Membership.mem (γ := Submodule ℝ ℝ[X]) (degreeLT ℝ (2 * n)) P
Tactic: have hmem : P ∈ degreeLT ℝ (2 * n) := by rwa [mem_degreeLT]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
hmem : Membership.mem (γ := Submodule ℝ ℝ[X]) (degreeLT ℝ (2 * n)) P
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
have hmem₁ : ∃ (c : ℕ → ℝ), ∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) = P
Tactic: rw [← Sequence.span_degreeLT (chebyshevTsequence ℝ) (by simp),
    show Set.Iio (2 * n) = Finset.range (2 * n) by simp,
    Submodule.mem_span_image_finset_iff_exists_fun'] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
hmem : ∃ (c : ℕ → ℝ), ∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) = P
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P
have obtain : ∀ (c : ℕ → ℝ)
  (hP :
    degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
      HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)),
  ∫ (x : ℝ),
      eval x (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))
Tactic: obtain ⟨c, rfl⟩ := hmem
Cleared hypotheses: P, hP, hmem
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ ∫ (x : ℝ),
      eval x (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))
have simp_rw : ∫ (x : ℝ), ∑ x_1 ∈ range (2 * n), c x_1 • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x_1) ∂measureT =
  sumZeroes n (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))
Tactic: simp_rw [eval_finsetSum, eval_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ ∫ (x : ℝ), ∑ x_1 ∈ range (2 * n), c x_1 • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x_1) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))
have rw : Eq (α := ℝ) (∑ i ∈ range (2 * n), ∫ (a : ℝ), c i • eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) ∂measureT)
  (∑ i ∈ range (2 * n), sumZeroes n (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)))
Tactic: rw [MeasureTheory.integral_finsetSum, sumZeroes_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
rw :
  Eq (α := ℝ) (∑ i ∈ range (2 * n), ∫ (a : ℝ), c i • eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) ∂measureT)
    (∑ i ∈ range (2 * n), sumZeroes n (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)))
⊢ ∫ (x : ℝ), ∑ x_1 ∈ range (2 * n), c x_1 • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x_1) ∂measureT =
    sumZeroes n (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))
have hf : ∀ i ∈ range (2 * n),
  MeasureTheory.Integrable (ε := ℝ) (fun (x : ℝ) ↦ c i • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) measureT
Tactic: rw [MeasureTheory.integral_finsetSum, sumZeroes_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ Eq (α := ℝ) (∑ i ∈ range (2 * n), ∫ (a : ℝ), c i • eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) ∂measureT)
    (∑ i ∈ range (2 * n), sumZeroes n (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)))
have simp_rw : Eq (α := ℝ) (∑ x ∈ range (2 * n), c x * ∫ (a : ℝ), eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x) ∂measureT)
  (∑ x ∈ range (2 * n), c x * sumZeroes n ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x))
Tactic: simp_rw [sumZeroes_smul, smul_eq_mul, MeasureTheory.integral_const_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ Eq (α := ℝ) (∑ x ∈ range (2 * n), c x * ∫ (a : ℝ), eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x) ∂measureT)
    (∑ x ∈ range (2 * n), c x * sumZeroes n ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) x))
have a : ∀ (i : ℕ) (hrange : i ∈ range (2 * n)),
  ∫ (a : ℝ), eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) ∂measureT =
    sumZeroes n ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)
Tactic: congr! with i hrange
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have pos : i = 0 → ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
Tactic: by_cases i = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
pos : i = 0 → ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have neg : ¬i = 0 → ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
Tactic: by_cases i = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have rw : ∫ (a : ℝ), eval a (T ℝ (↑0 : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑0 : ℤ))
Tactic: rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
rw : ∫ (a : ℝ), eval a (T ℝ (↑0 : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑0 : ℤ))
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have rw₁ : ∫ (a : ℝ), eval a (T ℝ 0) ∂measureT = sumZeroes n (T ℝ 0)
Tactic: rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
rw : ∫ (a : ℝ), eval a (T ℝ (↑0 : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑0 : ℤ))
rw₁ : ∫ (a : ℝ), eval a (T ℝ 0) ∂measureT = sumZeroes n (T ℝ 0)
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have rw₂ : π = sumZeroes n (T ℝ 0)
Tactic: rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : i = 0
rw : ∫ (a : ℝ), eval a (T ℝ (↑0 : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑0 : ℤ))
rw₁ : ∫ (a : ℝ), eval a (T ℝ 0) ∂measureT = sumZeroes n (T ℝ 0)
rw₂ : π = sumZeroes n (T ℝ 0)
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have rw₃ : π = π
Tactic: rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ (↑i : ℤ)
have refine : (↑i : ℤ) < HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) 0 1
Tactic: refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ (↑i : ℤ) < HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) 0 1
have rw_mod_cast : ∀
  (hP :
    degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
      (↑(2 * n) : WithBot ℕ)),
  i < 2 * n
Tactic: rw_mod_cast [zero_add, mul_one]
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have this : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ (↑i : ℤ)
Tactic: have : ¬ (2 * n : ℤ) ∣ i := by
        refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩
        rw_mod_cast [zero_add, mul_one]
        exact mem_range.mp hrange
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ (↑i : ℤ)
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have rw : 0 = sumZeroes n (T ℝ (↑i : ℤ))
Tactic: rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ (↑i : ℤ)
rw : 0 = sumZeroes n (T ℝ (↑i : ℤ))
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ ∀ i ∈ range (2 * n),
    MeasureTheory.Integrable (ε := ℝ) (fun (x : ℝ) ↦ c i • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) measureT
have hf : ∀ i ∈ range (2 * n),
  MeasureTheory.Integrable (ε := ℝ)
    (fun (x : ℝ) ↦ eval x (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))) measureT
Tactic: simp_rw [← eval_smul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
⊢ node n n = -1
have this : (↑n : ℝ) * π / (↑n : ℝ) = π
Tactic: have : n * π / n = π := by aesop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have inl : ∀ (hi : Membership.mem (γ := Finset ℕ) (Finset.Iic 0) i), eval (node 0 i) (T ℝ (↑0 : ℤ)) = HPow.hPow (α := ℝ) (-1) i
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
inl :
  ∀ (hi : Membership.mem (γ := Finset ℕ) (Finset.Iic 0) i), eval (node 0 i) (T ℝ (↑0 : ℤ)) = HPow.hPow (α := ℝ) (-1) i
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have inr : ∀ (hn : n ≠ 0), eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have this : (↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π
Tactic: have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : (↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have inr : eval (cos ((↑i : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
Tactic: rw [node, T_real_cos, this, cos_nat_mul_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : (↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π
inr : eval (cos ((↑i : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have inr₁ : cos ((↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (-1) i
Tactic: rw [node, T_real_cos, this, cos_nat_mul_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : (↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π
inr : eval (cos ((↑i : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
inr₁ : cos ((↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (-1) i
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have inr₂ : cos ((↑i : ℝ) * π) = HPow.hPow (α := ℝ) (-1) i
Tactic: rw [node, T_real_cos, this, cos_nat_mul_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
this : (↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π
inr : eval (cos ((↑i : ℝ) * π / (↑n : ℝ))) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
inr₁ : cos ((↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ))) = HPow.hPow (α := ℝ) (-1) i
inr₂ : cos ((↑i : ℝ) * π) = HPow.hPow (α := ℝ) (-1) i
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
have inr₃ : HPow.hPow (α := ℝ) (-1) i = HPow.hPow (α := ℝ) (-1) i
Tactic: rw [node, T_real_cos, this, cos_nat_mul_pi]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)
have inl : StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node 0 x) (↑(Finset.range (HAdd.hAdd (α := ℕ) 0 1)) : Set ℕ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
inl : StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node 0 x) (↑(Finset.range (HAdd.hAdd (α := ℕ) 0 1)) : Set ℕ)
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)
have inr : ∀ (hn : n ≠ 0), StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)
have inr : StrictMonoOn (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)) (↑(Finset.range (n + 1)) : Set ℕ)
Tactic: refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
hn : n ≠ 0
inr : StrictMonoOn (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)) (↑(Finset.range (n + 1)) : Set ℕ)
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)
have inr₁ : ∀ (x : ℕ) (hx : x ∈ (↑(Finset.range (n + 1)) : Set ℕ)), (↑x : ℝ) * π / (↑n : ℝ) ≤ π
Tactic: refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ StrictMonoOn (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)) (↑(Finset.range (n + 1)) : Set ℕ)
have inr : StrictMono (β := ℝ) fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)
Tactic: apply StrictMono.strictMonoOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ∈ (↑(Finset.range (n + 1)) : Set ℕ)
⊢ (↑x : ℝ) * π / (↑n : ℝ) ≤ π
have hx₁ : x ≤ n
Tactic: rw [Finset.mem_coe, Finset.mem_range_succ_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
⊢ (↑x : ℝ) * π / (↑n : ℝ) ≤ π
have inr : (↑x : ℝ) * (π / (↑n : ℝ)) ≤ π
Tactic: rw [mul_div_assoc]