awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1
m : ℤ
hx : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I = (↑m : ℂ) * (2 * (↑π : ℂ) * I)
⊢ (↑k : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
      ((↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ) +
        HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
    0
have a : (↑k : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
    (HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑m : ℂ) +
      HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
  0
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1
m : ℤ
hx : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I = (↑m : ℂ) * (2 * (↑π : ℂ) * I)
⊢ Eq (α := ℂ) (↑k : ℂ) (↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ)
have a : (↑k : ℂ) + (↑m : ℂ) * (2 * (↑π : ℂ) * I) * ((↑n : ℂ) / (↑π : ℂ) / I) -
    ((↑(HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m) : ℂ) +
      HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I * ((↑n : ℂ) / (↑π : ℂ) / I)) =
  0
Tactic: linear_combination (norm := (push_cast; field [show (n : ℂ) ≠ 0 by aesop])) hx * (n / π / I)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = 1
m : ℤ
hx : HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I = (↑m : ℂ) * (2 * (↑π : ℂ) * I)
⊢ HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
have h : k = HMul.hMul (α := ℤ) 2 (↑n : ℤ) * m
Tactic: have h : k = 2 * n * m := by
    apply (@Int.cast_inj ℂ _ _).mp
    linear_combination (norm := (push_cast; field [show (n : ℂ) ≠ 0 by aesop])) hx * (n / π / I)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
⊢ ∑ i ∈ range n,
      Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) =
    Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I) /
        (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) *
      (HPow.hPow (α := ℂ) (-1) k - 1)
have this₁ : (∑ i ∈ range n,
        Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
      (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
    (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
  HPow.hPow (α := ℂ) (-1) k - 1
Tactic: rw [Complex.exp_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
s a b t : ℂ
h : s * a⁻¹ * b = t
ha : a ≠ 0
hb : b ≠ 0
⊢ s = a / b * t
have a₁ : s + t * a / b - (a / b * t + s * a⁻¹ * b * a / b) = 0
Tactic: linear_combination (norm := field) h * a / b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
this :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        (Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))⁻¹ *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
⊢ ∑ i ∈ range n,
      Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) =
    Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I) /
        (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) *
      (HPow.hPow (α := ℂ) (-1) k - 1)
have hf : ∀ {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0), s = a / b * t
Tactic: have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ ∑ i ∈ range n,
      Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) =
    Complex.exp ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I) /
        (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) *
      (HPow.hPow (α := ℂ) (-1) k - 1)
have suffices : (∑ i ∈ range n,
        Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
      Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
    (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
  HPow.hPow (α := ℂ) (-1) k - 1
Tactic: suffices (∑ i ∈ range n, exp ((k * ((2 * i + 1) / (2 * n) * π)) * I)) *
    exp (-(k / (2 * n) * π * I)) * (exp (k / n * π * I) - 1) = (-1) ^ k - 1 by
    rw [Complex.exp_neg] at this
    have hf {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0) : s = a / b * t := by
      linear_combination (norm := field) h * a / b
    apply hf this (Complex.exp_ne_zero _) (by grind [exp_sub_one_ne_zero])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
have h : (∑ i ∈ range n,
        Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
      Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
    (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
  (∑ i ∈ range n, Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i) *
    (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1)
Tactic: convert! geom_sum_mul (exp (k / n * π * I)) n using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
h :
  (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    (∑ i ∈ range n, Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1)
⊢ (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    HPow.hPow (α := ℂ) (-1) k - 1
have h₁ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 1
Tactic: convert! geom_sum_mul (exp (k / n * π * I)) n using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ (∑ i ∈ range n,
          Complex.exp
            ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I)) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    (∑ i ∈ range n, Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1)
have h : Eq (α := ℂ)
  (∑ i ∈ range n,
    Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1))
  (∑ i ∈ range n,
    Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1))
Tactic: simp_rw [sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ Eq (α := ℂ)
    (∑ i ∈ range n,
      Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) *
          Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
        (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1))
    (∑ i ∈ range n,
      Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i *
        (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1))
have h : ∀ (i : ℕ) (hi : i ∈ range n),
  Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1)
Tactic: congr! 1 with i hi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
i : ℕ
hi : i ∈ range n
⊢ Complex.exp ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I) *
        Complex.exp (-((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1)
have h : Complex.exp
      ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ)) * I +
        -((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I)) *
    (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
  Complex.exp ((↑i : ℂ) * (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I)) *
    (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1)
Tactic: rw [← Complex.exp_nat_mul, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 1
have h : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑n : ℂ) * (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I)) - 1
Tactic: rw [← Complex.exp_nat_mul,
      show (n * (k / n * π * I)) = k * (π * I) by field [show (n : ℂ) ≠ 0 by aesop],
      Complex.exp_int_mul, Complex.exp_pi_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
h : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑n : ℂ) * (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I)) - 1
⊢ HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 1
have h₁ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑k : ℂ) * ((↑π : ℂ) * I)) - 1
Tactic: rw [← Complex.exp_nat_mul,
      show (n * (k / n * π * I)) = k * (π * I) by field [show (n : ℂ) ≠ 0 by aesop],
      Complex.exp_int_mul, Complex.exp_pi_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
h : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑n : ℂ) * (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I)) - 1
h₁ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑k : ℂ) * ((↑π : ℂ) * I)) - 1
⊢ HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 1
have h₂ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑π : ℂ) * I) ^ k - 1
Tactic: rw [← Complex.exp_nat_mul,
      show (n * (k / n * π * I)) = k * (π * I) by field [show (n : ℂ) ≠ 0 by aesop],
      Complex.exp_int_mul, Complex.exp_pi_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
h : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑n : ℂ) * (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I)) - 1
h₁ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑k : ℂ) * ((↑π : ℂ) * I)) - 1
h₂ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp ((↑π : ℂ) * I) ^ k - 1
⊢ HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 1
have h₃ : HPow.hPow (α := ℂ) (-1) k - 1 = HPow.hPow (α := ℂ) (-1) k - 1
Tactic: rw [← Complex.exp_nat_mul,
      show (n * (k / n * π * I)) = k * (π * I) by field [show (n : ℂ) ≠ 0 by aesop],
      Complex.exp_int_mul, Complex.exp_pi_mul_I]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, sumZeroes n (P i)
have simp_rw : π / (↑n : ℝ) *
    ∑ x ∈ range n, ∑ i ∈ s, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P i) =
  ∑ x ∈ s,
    π / (↑n : ℝ) *
      ∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P x)
Tactic: simp_rw [sumZeroes, eval_finsetSum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
⊢ π / (↑n : ℝ) *
      ∑ x ∈ range n,
        ∑ i ∈ s, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P i) =
    ∑ x ∈ s,
      π / (↑n : ℝ) *
        ∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P x)
have rw : π / (↑n : ℝ) *
    ∑ y ∈ s, ∑ x ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P y) =
  ∑ x ∈ s,
    π / (↑n : ℝ) *
      ∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P x)
Tactic: rw [sum_comm, mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
rw :
  π / (↑n : ℝ) *
      ∑ y ∈ s,
        ∑ x ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P y) =
    ∑ x ∈ s,
      π / (↑n : ℝ) *
        ∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P x)
⊢ π / (↑n : ℝ) *
      ∑ x ∈ range n,
        ∑ i ∈ s, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P i) =
    ∑ x ∈ s,
      π / (↑n : ℝ) *
        ∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P x)
have rw₁ : Eq (α := ℝ)
  (∑ i ∈ s,
    π / (↑n : ℝ) *
      ∑ x ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P i))
  (∑ x ∈ s,
    π / (↑n : ℝ) *
      ∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (P x))
Tactic: rw [sum_comm, mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
c : ℝ
P : ℝ[X]
⊢ sumZeroes n (c • P) = c * sumZeroes n P
have simp_rw : π / (↑n : ℝ) *
    (c * ∑ x ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) P) =
  c *
    (π / (↑n : ℝ) *
      ∑ x ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑x : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) P)
Tactic: simp_rw [sumZeroes, eval_smul, ← smul_sum, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ sumZeroes n (T ℝ k) = 0
have inl : ∀ (hk : ¬HMul.hMul (α := ℤ) 2 (↑0 : ℤ) ∣ k), sumZeroes 0 (T ℝ k) = 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n, hk
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
inl : ∀ (hk : ¬HMul.hMul (α := ℤ) 2 (↑0 : ℤ) ∣ k), sumZeroes 0 (T ℝ k) = 0
⊢ sumZeroes n (T ℝ k) = 0
have inr : ∀ (hn : n ≠ 0), sumZeroes n (T ℝ k) = 0
Tactic: rcases eq_or_ne n 0 with rfl | hn
-- 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 :
  Eq (α := ℝ)
    (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0
⊢ sumZeroes n (T ℝ k) = 0
have rw : Eq (α := ℝ)
  (∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (T ℝ k)) 0
Tactic: rw [sumZeroes, mul_eq_zero_iff_left (by aesop)]
-- 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 :
  Eq (α := ℝ)
    (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0
⊢ Eq (α := ℝ)
    (∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (T ℝ k)) 0
have this₁ : Eq (α := ℝ) (∑ i ∈ range n, cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)))
  0
Tactic: rw [← mul_sum, mul_eq_zero_iff_left (by norm_num)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ sumZeroes n (T ℝ k) = 0
have inr : Eq (α := ℝ)
  (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0
Tactic: suffices ∑ i ∈ range n, 2 * cos (k * ((2 * i + 1) / (2 * n) * π)) = 0 by
    rw [sumZeroes, mul_eq_zero_iff_left (by aesop)]
    rw [← mul_sum, mul_eq_zero_iff_left (by norm_num)] at this
    simpa [T_real_cos]
-- 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 :
  Eq (α := ℂ)
    (∑ i ∈ range n,
      2 * (↑(cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) : ℂ))
    0
⊢ Eq (α := ℝ)
    (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0
have norm_cast : ∀
  (this :
    Eq (α := ℝ) (∑ x ∈ range n, 2 * cos ((↑k : ℝ) * (HDiv.hDiv (α := ℝ) (↑(2 * x + 1) : ℝ) (↑(2 * n) : ℝ) * π))) 0),
  Eq (α := ℝ) (∑ x ∈ range n, 2 * cos ((↑k : ℝ) * (HDiv.hDiv (α := ℝ) (↑(2 * x + 1) : ℝ) (↑(2 * n) : ℝ) * π))) 0
Tactic: norm_cast at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ Eq (α := ℝ)
    (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0
have inr : Eq (α := ℂ)
  (∑ i ∈ range n,
    2 * (↑(cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) : ℂ))
  0
Tactic: suffices (∑ i ∈ range n, 2 * cos (k * ((2 * i + 1) / (2 * n) * π)) : ℂ) = 0 by norm_cast at this ⊢
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ Eq (α := ℂ)
    (∑ i ∈ range n,
      2 * (↑(cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) : ℂ))
    0
have inr : Eq (α := ℂ)
  (∑ i ∈ range n,
    2 * Complex.cos ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ))))
  0
Tactic: suffices ∑ i ∈ range n, 2 * Complex.cos (k * ((2 * i + 1) / (2 * n) * π)) = 0 by aesop
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ Eq (α := ℂ)
    (∑ i ∈ range n,
      2 * Complex.cos ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ))))
    0
have inr : 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
Tactic: simp_rw [Complex.two_cos, ← neg_mul, ← Int.cast_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (goal)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
have rw : Eq (α := ℂ) (↑(↑(-k).negOnePow : ℤ) : ℂ) (↑(↑k.negOnePow : ℤ) : ℂ)
Tactic: rw [← Int.cast_negOnePow, ← Int.cast_negOnePow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss (hypothesis)
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ 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 this : HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k
Tactic: have : (-1 : ℂ) ^ (-k) = (-1) ^ k := by rw [← Int.cast_negOnePow, ← Int.cast_negOnePow]; simp