awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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

Tactic:
have hz₂ : exp (k / n * π * I) = z ^ 2 := by rw [hz, ← Complex.exp_nat_mul]; grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
inr : z / (HPow.hPow (β := ℕ) z 2 - 1) + z⁻¹ / (HPow.hPow (β := ℕ) z⁻¹ 2 - 1) = 0
⊢ z / (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) +
      z⁻¹ / ((Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ - 1) =
    0

Tactic:
rw [hz₂, ← inv_pow z 2]

Premises used: inv_pow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 ≠ 0

Tactic:
grind [Complex.exp_ne_zero]

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
⊢ HPow.hPow (β := ℕ) z 2 - 1 ≠ 0 ∧ 1 - HPow.hPow (β := ℕ) z 2 ≠ 0

Tactic:
grind [exp_sub_one_ne_zero]

Premises used: _private.0.Polynomial.Chebyshev.exp_sub_one_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 / (HPow.hPow (β := ℕ) z 2 - 1) + z⁻¹ / (HPow.hPow (β := ℕ) z⁻¹ 2 - 1) = 0

Tactic:
field [show z ≠ 0 by grind [Complex.exp_ne_zero],
    show (z ^ 2 - 1 ≠ 0) ∧ (1 - z ^ 2 ≠ 0) by grind [exp_sub_one_ne_zero]]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
rwa rwa₁ rwa₂ rwa₃ : P.degree < (↑(2 * n) : WithBot ℕ)
⊢ Membership.mem (γ := Submodule ℝ ℝ[X]) (degreeLT ℝ (2 * n)) P

Tactic:
rwa [mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
⊢ Membership.mem (γ := Submodule ℝ ℝ[X]) (degreeLT ℝ (2 * n)) P

Tactic:
have hmem : P ∈ degreeLT ℝ (2 * n) := by rwa [mem_degreeLT]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
⊢ ∀ i < 2 * n, IsUnit (leadingCoeff ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < HMul.hMul (α := WithBot ℕ) 2 (↑n : WithBot ℕ)
hmem :
  Membership.mem (γ := Submodule ℝ ℝ[X]) (Submodule.span ℝ ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) '' Set.Iio (2 * n))) P
⊢ Set.Iio (2 * n) = (↑(range (2 * n)) : Set ℕ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
⊢ ∃ (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

Premises used: Real, Polynomial.Chebyshev.chebyshevTsequence, Submodule.mem_span_image_finset_iff_exists_fun', Polynomial.Sequence.span_degreeLT
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
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))
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
obtain ⟨c, rfl⟩ := hmem

Premises used: rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 ℕ)
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))
⊢ ∫ (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:
simp_rw [eval_finsetSum, eval_smul]

Premises used: Polynomial.eval_finsetSum, Polynomial.eval_smul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)))
hf :
  ∀ i ∈ range (2 * n),
    MeasureTheory.Integrable (ε := ℝ) (fun (x : ℝ) ↦ c i • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) measureT
⊢ ∫ (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:
rw [MeasureTheory.integral_finsetSum, sumZeroes_sum]

Premises used: MeasureTheory.integral_finsetSum, Polynomial.Chebyshev.sumZeroes_sum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 ℕ)
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))
⊢ 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:
simp_rw [sumZeroes_smul, smul_eq_mul, MeasureTheory.integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, smul_eq_mul, Polynomial.Chebyshev.sumZeroes_smul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 ℕ)
a :
  ∀ (i : ℕ) (hrange : i ∈ range (2 * n)),
    ∫ (a : ℝ), eval a ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i) ∂measureT =
      sumZeroes n ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)
⊢ 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:
congr! with i hrange
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℤ))
neg : ¬i = 0 → ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))

Tactic:
by_cases i = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
rw₃ rw₄ : π = π
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))

Tactic:
rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]

Premises used: Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, Polynomial.Chebyshev.sumZeroes_T_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
h : i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))

Tactic:
case pos hi => rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]

Premises used: Polynomial.Chebyshev.integral_eval_T_real_measureT_zero, Polynomial.Chebyshev.sumZeroes_T_zero, Nat.cast_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
⊢ 0 < HMul.hMul (α := ℤ) 2 (↑n : ℤ)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℤ) * 0 < (↑i : ℤ)

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
refine : (↑i : ℤ) < HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) 0 1
⊢ ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ (↑i : ℤ)

Tactic:
refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩

Premises used: Iff.mpr, Int.not_dvd_iff_lt_mul_succ, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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_mod_cast :
  ∀
    (hP :
      degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
        (↑(2 * n) : WithBot ℕ)),
    i < 2 * n
⊢ (↑i : ℤ) < HMul.hMul (α := ℤ) 2 (↑n : ℤ) * HAdd.hAdd (α := ℤ) 0 1

Tactic:
rw_mod_cast [zero_add, mul_one]

Premises used: zero_add, mul_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
hn : ¬n = 0
c : ℕ → ℝ
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    (↑(2 * n) : WithBot ℕ)
⊢ i < 2 * n

Tactic:
mem_range.mp hrange

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
hn : ¬n = 0
c : ℕ → ℝ
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
hP :
  degree (R := ℝ) (∑ i ∈ range (2 * n), HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) <
    (↑(2 * n) : WithBot ℕ)
⊢ i < 2 * n

Tactic:
exact mem_range.mp hrange

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℤ)

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
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℤ)
⊢ Ne (α := ℤ) (↑i : ℤ) 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℤ))
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ∫ (a : ℝ), eval a (T ℝ (↑i : ℤ)) ∂measureT = sumZeroes n (T ℝ (↑i : ℤ))

Tactic:
rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]

Premises used: Polynomial.Chebyshev.sumZeroes_T_of_not_dvd, Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 ℕ)
hf :
  ∀ i ∈ range (2 * n),
    MeasureTheory.Integrable (ε := ℝ)
      (fun (x : ℝ) ↦ eval x (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))) measureT
⊢ ∀ i ∈ range (2 * n),
    MeasureTheory.Integrable (ε := ℝ) (fun (x : ℝ) ↦ c i • eval x ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)) measureT

Tactic:
simp_rw [← eval_smul]

Premises used: Polynomial.eval_smul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℕ
hi : i ∈ range (2 * n)
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ eval x (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i)))
    (Set.Icc (-1) 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 : ℝ) ↦ eval x (HSMul.hSMul (β := ℝ[X]) (c i) ((↑(chebyshevTsequence ℝ) : ℕ → ℝ[X]) i))) measureT

Tactic:
exact fun i hi => integrable_measureT (by fun_prop)

Premises used: Polynomial.Chebyshev.integrable_measureT
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
⊢ node n 0 = 1

Tactic:
simp [node]

Premises used: Polynomial.Chebyshev.node
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n : ℝ) * π / (↑n : ℝ) = π

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
⊢ (↑n : ℝ) * π / (↑n : ℝ) = π

Tactic:
have : n * π / n = π := by aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
this : (↑n : ℝ) * π / (↑n : ℝ) = π
⊢ node n n = -1

Tactic:
simp [node, this]

Premises used: Polynomial.Chebyshev.node
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i : ℕ
⊢ Membership.mem (γ := Set ℝ) (Set.Icc (-1) 1) (node n i)

Tactic:
Set.mem_Icc.mpr ⟨neg_one_le_cos _, cos_le_one _⟩

Premises used: Iff.mpr, Real.neg_one_le_cos, And.intro, Set.mem_Icc, Real.cos_le_one
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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
inr : ∀ (hn : n ≠ 0), eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
i : ℕ
hi : Membership.mem (γ := Finset ℕ) (Finset.Iic 0) i
⊢ i = 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
i : ℕ
hi : Membership.mem (γ := Finset ℕ) (Finset.Iic 0) i
⊢ eval (node 0 i) (T ℝ (↑0 : ℤ)) = HPow.hPow (α := ℝ) (-1) i

Tactic:
simp [show i = 0 by grind]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ (↑n : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n i : ℕ
hi : i ∈ Finset.Iic n
hn : n ≠ 0
⊢ (↑(↑n : ℤ) : ℝ) * ((↑i : ℝ) * π / (↑n : ℝ)) = (↑i : ℝ) * π

Tactic:
have : (n : ℤ) * (i * π / n) = i * π := by norm_cast; field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
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
inr₃ inr₄ : HPow.hPow (α := ℝ) (-1) i = HPow.hPow (α := ℝ) (-1) i
⊢ eval (node n i) (T ℝ (↑n : ℤ)) = HPow.hPow (α := ℝ) (-1) i

Tactic:
rw [node, T_real_cos, this, cos_nat_mul_pi]

Premises used: Real.cos_nat_mul_pi, Polynomial.Chebyshev.node, Polynomial.Chebyshev.T_real_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
inl : StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node 0 x) (↑(Finset.range (HAdd.hAdd (α := ℕ) 0 1)) : Set ℕ)
inr : ∀ (hn : n ≠ 0), StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node 0 x) (↑(Finset.range (HAdd.hAdd (α := ℕ) 0 1)) : Set ℕ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ∈ (↑(Finset.range (n + 1)) : Set ℕ)
⊢ 0 ≤ (↑x : ℝ) * π / (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
inr : StrictMonoOn (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)) (↑(Finset.range (n + 1)) : Set ℕ)
inr₁ : ∀ (x : ℕ) (hx : x ∈ (↑(Finset.range (n + 1)) : Set ℕ)), (↑x : ℝ) * π / (↑n : ℝ) ≤ π
⊢ StrictAntiOn (β := ℝ) (fun (x : ℕ) ↦ node n x) (↑(Finset.range (n + 1)) : Set ℕ)

Tactic:
refine strictAntiOn_cos.comp_strictMonoOn ?_ (fun x hx => Set.mem_Icc.mpr ⟨by positivity, ?_⟩)

Premises used: Iff.mpr, StrictAntiOn.comp_strictMonoOn, And.intro, Set.mem_Icc, Real.strictAntiOn_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
inr : StrictMono (β := ℝ) fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)
⊢ StrictMonoOn (β := ℝ) (fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)) (↑(Finset.range (n + 1)) : Set ℕ)

Tactic:
apply StrictMono.strictMonoOn

Premises used: StrictMono.strictMonoOn
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
⊢ 0 < π

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
⊢ StrictMono (β := ℝ) fun (x : ℕ) ↦ (↑x : ℝ) * π / (↑n : ℝ)

Tactic:
exact StrictMono.mul_const
      (StrictMono.mul_const Nat.strictMono_cast (by positivity)) (by positivity)

Premises used: Nat.strictMono_cast, StrictMono.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ∈ (↑(Finset.range (n + 1)) : Set ℕ)
⊢ x ≤ n

Tactic:
rw [Finset.mem_coe, Finset.mem_range_succ_iff] at hx

Premises used: Finset.mem_range_succ_iff, Finset.mem_coe
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
inr : (↑x : ℝ) * (π / (↑n : ℝ)) ≤ π
⊢ (↑x : ℝ) * π / (↑n : ℝ) ≤ π

Tactic:
rw [mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Goal:
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
inr : (↑x : ℝ) * (π / (↑n : ℝ)) ≤ (↑n : ℝ) * (π / (↑n : ℝ))
⊢ (↑x : ℝ) * (π / (↑n : ℝ)) ≤ π

Tactic:
nth_rewrite 2 [← mul_div_cancel₀ π (Nat.cast_ne_zero.mpr hn)]

Premises used: Iff.mpr, Real.pi, mul_div_cancel₀, Nat.cast_ne_zero