awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
hf : ∀ {s a b t : ℂ} (h : s * a⁻¹ * b = t) (ha : a ≠ 0) (hb : b ≠ 0), s = a / b * t
⊢ ∑ 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:
apply hf this (Complex.exp_ne_zero _) (by grind [exp_sub_one_ne_zero])

Premises used: Complex.exp_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
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
⊢ ∑ 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])
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ (∑ i ∈ range n, Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ i) *
      (Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) - 1) =
    Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 1

Tactic:
geom_sum_mul (exp (k / n * π * I)) n

Premises used: Int.cast, Real.pi, HMul.hMul, HDiv.hDiv, geom_sum_mul, Complex.ofReal, Nat.cast, Complex.exp, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
h₁ : HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 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

Tactic:
convert! geom_sum_mul (exp (k / n * π * I)) n using 1

Premises used: Int.cast, Real.pi, HMul.hMul, HDiv.hDiv, geom_sum_mul, Complex.ofReal, Nat.cast, Complex.exp, Complex.I
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
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))
⊢ (∑ 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]

Premises used: Finset.sum_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
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)
⊢ 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:
congr! 1 with i hi
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
i : ℕ
hi : i ∈ range n
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)
⊢ 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:
rw [← Complex.exp_nat_mul, ← Complex.exp_add]

Premises used: Complex.exp_add, Complex.exp_nat_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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 +
          -((↑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:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ Ne (α := ℂ) (↑n : ℂ) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hn : n ≠ 0
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
⊢ (↑n : ℂ) * (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = (↑k : ℂ) * ((↑π : ℂ) * I)

Tactic:
field [show (n : ℂ) ≠ 0 by aesop]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
h₃ h₄ : HPow.hPow (α := ℂ) (-1) k - 1 = HPow.hPow (α := ℂ) (-1) k - 1
⊢ HPow.hPow (α := ℂ) (-1) k - 1 = Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) ^ n - 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]

Premises used: Complex.exp_pi_mul_I, Complex.exp_nat_mul, Complex.exp_int_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
ι : Type u_1
s : Finset ι
P : ι → ℝ[X]
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)
⊢ sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, sumZeroes n (P i)

Tactic:
simp_rw [sumZeroes, eval_finsetSum]

Premises used: Polynomial.Chebyshev.sumZeroes, Polynomial.eval_finsetSum
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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)
rw₁ 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))
⊢ π / (↑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:
rw [sum_comm, mul_sum]

Premises used: Finset.mul_sum, Finset.sum_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
c : ℝ
P : ℝ[X]
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)
⊢ sumZeroes n (c • P) = c * sumZeroes n P

Tactic:
simp_rw [sumZeroes, eval_smul, ← smul_sum, smul_eq_mul]

Premises used: Polynomial.Chebyshev.sumZeroes, Finset.smul_sum, Polynomial.eval_smul, smul_eq_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
c : ℝ
P : ℝ[X]
⊢ π / (↑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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
hn : n ≠ 0
⊢ π / (↑n : ℝ) * (↑n : ℝ) = π

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
hn : n ≠ 0
⊢ sumZeroes n (T ℝ 0) = π

Tactic:
simp [sumZeroes, show π / n * n = π by field]

Premises used: Polynomial.Chebyshev.sumZeroes
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
inl : ∀ (hk : ¬HMul.hMul (α := ℤ) 2 (↑0 : ℤ) ∣ k), sumZeroes 0 (T ℝ k) = 0
inr : ∀ (hn : n ≠ 0), sumZeroes n (T ℝ k) = 0
⊢ sumZeroes n (T ℝ k) = 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑0 : ℤ) ∣ k
⊢ sumZeroes 0 (T ℝ k) = 0

Tactic:
simp [sumZeroes]

Premises used: Polynomial.Chebyshev.sumZeroes
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
⊢ π / (↑n : ℝ) ≠ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
rw :
  Eq (α := ℝ)
    (∑ i ∈ range n, eval (cos ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π)) (T ℝ k)) 0
⊢ sumZeroes n (T ℝ k) = 0

Tactic:
rw [sumZeroes, mul_eq_zero_iff_left (by aesop)]

Premises used: Polynomial.Chebyshev.sumZeroes, mul_eq_zero_iff_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this :
  HMul.hMul (α := ℝ) 2
      (∑ i ∈ range n, cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) =
    0
⊢ Ne (α := ℝ) 2 0

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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, 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

Premises used: Finset.mul_sum, mul_eq_zero_iff_left
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this :
  Eq (α := ℝ)
    (∑ i ∈ range n, 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

Tactic:
simpa [T_real_cos]

Premises used: Polynomial.Chebyshev.T_real_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
inr :
  Eq (α := ℝ)
    (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0
⊢ sumZeroes n (T ℝ k) = 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]
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
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
norm_cast norm_cast₁ norm_cast₂ 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
⊢ Eq (α := ℝ)
    (∑ i ∈ range n, 2 * cos ((↑k : ℝ) * ((HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) / HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π))) 0

Tactic:
norm_cast at this ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
inr :
  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

Tactic:
suffices (∑ i ∈ range n, 2 * cos (k * ((2 * i + 1) / (2 * n) * π)) : ℂ) = 0 by norm_cast at this ⊢
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
this :
  Eq (α := ℂ)
    (∑ i ∈ range n,
      2 * Complex.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

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
inr :
  Eq (α := ℂ)
    (∑ i ∈ range n,
      2 * Complex.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

Tactic:
suffices ∑ i ∈ range n, 2 * Complex.cos (k * ((2 * i + 1) / (2 * n) * π)) = 0 by aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
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
⊢ Eq (α := ℂ)
    (∑ i ∈ range n,
      2 * Complex.cos ((↑k : ℂ) * ((HMul.hMul (α := ℂ) 2 (↑i : ℂ) + 1) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ))))
    0

Tactic:
simp_rw [Complex.two_cos, ← neg_mul, ← Int.cast_neg]

Premises used: Int.cast_neg, neg_mul, Complex.two_cos
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
rw : Eq (α := ℂ) (↑(↑(-k).negOnePow : ℤ) : ℂ) (↑(↑k.negOnePow : ℤ) : ℂ)
⊢ HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k

Tactic:
rw [← Int.cast_negOnePow, ← Int.cast_negOnePow]

Premises used: Int.cast_negOnePow
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ Eq (α := ℂ) (↑(↑(-k).negOnePow : ℤ) : ℂ) (↑(↑k.negOnePow : ℤ) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Goal:
n : ℕ
k : ℤ
hk : ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ k
hn : n ≠ 0
⊢ HPow.hPow (α := ℂ) (-1) (-k) = HPow.hPow (α := ℂ) (-1) k

Tactic:
have : (-1 : ℂ) ^ (-k) = (-1) ^ k := by rw [← Int.cast_negOnePow, ← Int.cast_negOnePow]; simp
-- 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
⊢ ¬HMul.hMul (α := ℤ) 2 (↑n : ℤ) ∣ -k

Tactic:
aesop
-- 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
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
⊢ 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:
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]

Premises used: add_mul, Int.cast_neg, neg_div, Finset.sum_add_distrib, mul_eq_zero_of_left, Complex.exp_neg, neg_mul, _private.0.Polynomial.Chebyshev.sum_exp
-- 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
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
⊢ 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:
set z := exp (k / (2 * n) * π * I) with hz

Premises used: Int.cast, Real.pi, HMul.hMul, HDiv.hDiv, Complex.ofReal, Nat.cast, Complex.exp, OfNat.ofNat, Complex.I
-- 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)
rw :
  Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) =
    Complex.exp ((↑2 : ℂ) * ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))
⊢ Complex.exp (HDiv.hDiv (α := ℂ) (↑k : ℂ) (↑n : ℂ) * (↑π : ℂ) * I) = HPow.hPow (β := ℕ) z 2

Tactic:
rw [hz, ← Complex.exp_nat_mul]

Premises used: Complex.exp_nat_mul
-- 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) =
    Complex.exp ((↑2 : ℂ) * ((↑k : ℂ) / HMul.hMul (α := ℂ) 2 (↑n : ℂ) * (↑π : ℂ) * I))

Tactic:
grind