awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
hf₁ : (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)
h₁ : f = g₁ * p₁ * p₂
⊢ g₂ = p₁ * p₂

Tactic:
rw [h', ← mul_assoc] at h hf

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
hf₁ : (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)
h₁ : f = g₁ * p₁ * p₂
h'₁ : g₂ = p₁ * p₂
⊢ p₁.IsMonicOfDegree 1

Tactic:
rw [h', ← mul_assoc] at h hf

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
hf : (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)
h : f = g₁ * p₁ * p₂
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
⟨g₁ * p₁, p₂, hd₁.mul hp₁, (hd₁.mul hp₁).of_mul_left hf, h⟩

Premises used: HMul.hMul, Polynomial.IsMonicOfDegree.mul, Polynomial.IsMonicOfDegree.of_mul_left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
hf : (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)
h : f = g₁ * p₁ * p₂
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
exact ⟨g₁ * p₁, p₂, hd₁.mul hp₁, (hd₁.mul hp₁).of_mul_left hf, h⟩
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)

Tactic:
rw [h', mul_left_comm] at h hf

Premises used: mul_left_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
hf₁ : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
⊢ f = p₁ * (g₁ * p₂)

Tactic:
rw [h', mul_left_comm] at h hf

Premises used: mul_left_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
hf₁ : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
h₁ : f = p₁ * (g₁ * p₂)
⊢ g₂ = p₁ * p₂

Tactic:
rw [h', mul_left_comm] at h hf

Premises used: mul_left_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
hf₁ : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
h₁ : f = p₁ * (g₁ * p₂)
h'₁ : g₂ = p₁ * p₂
⊢ p₁.IsMonicOfDegree 2

Tactic:
rw [h', mul_left_comm] at h hf

Premises used: mul_left_comm
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
hf : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
h : f = p₁ * (g₁ * p₂)
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
⟨p₁, g₁ * p₂, hp₂, of_mul_left hp₂ hf, h⟩

Premises used: HMul.hMul, Polynomial.IsMonicOfDegree.of_mul_left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
hf : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
h : f = p₁ * (g₁ * p₂)
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
exact ⟨p₁, g₁ * p₂, hp₂, of_mul_left hp₂ hf, h⟩
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₂ : g₁.IsMonicOfDegree 2
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
⟨g₁, g₂, hd₂, of_mul_left hd₂ hf, h⟩

Premises used: Polynomial.IsMonicOfDegree.of_mul_left, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Polynomial.Factorization
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₂ : g₁.IsMonicOfDegree 2
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
exact ⟨g₁, g₂, hd₂, of_mul_left hd₂ hf, h⟩
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
⊢ Fact (0 < 2 * π)

Tactic:
Fact.mk Real.two_pi_pos

Premises used: Real.two_pi_pos, Fact.mk
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
⊢ Integrable (ε := ℂ) (α := AddCircle (2 * π))
    (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) : (a : AddCircle (2 * π)) → ℂ)
    haarAddCircle

Tactic:
simpa using p.toAddCircle.continuous.continuousOn.integrableOn_compact isCompact_univ

Premises used: ContinuousMap.continuous, Continuous.continuousOn, isCompact_univ, Polynomial.toAddCircle, ContinuousOn.integrableOn_compact, DFunLike.coe
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
c : ℂ
h :
  ∀ (θ : AddCircle (2 * π)),
    Eq (α := ℂ)
      ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((C : (a : ℂ) → ℂ[X]) c) : C(AddCircle (2 * π), ℂ)) :
            (a : AddCircle (2 * π)) → ℂ)
          θ :
        ℂ)
      ((HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier 0) : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)
⊢ (toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((C : (a : ℂ) → ℂ[X]) c) =
    HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier 0)

Tactic:
ext θ
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
c : ℂ
θ : AddCircle (2 * π)
⊢ Eq (α := ℂ)
    ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((C : (a : ℂ) → ℂ[X]) c) : C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        θ :
      ℂ)
    ((HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier 0) : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)

Tactic:
simp [toAddCircle]

Premises used: Polynomial.toAddCircle
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
h :
  ∀ (θ : AddCircle (2 * π)),
    Eq (α := ℂ)
      ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) X : C(AddCircle (2 * π), ℂ)) :
            (a : AddCircle (2 * π)) → ℂ)
          θ :
        ℂ)
      ((fourier 1 : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)
⊢ Eq (α := C(AddCircle (2 * π), ℂ)) ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) X : C(AddCircle (2 * π), ℂ))
    (fourier 1 : C(AddCircle (2 * π), ℂ))

Tactic:
ext θ
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
θ : AddCircle (2 * π)
⊢ Eq (α := ℂ)
    ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) X : C(AddCircle (2 * π), ℂ)) : (a : AddCircle (2 * π)) → ℂ)
        θ :
      ℂ)
    ((fourier 1 : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)

Tactic:
simp [toAddCircle]

Premises used: Polynomial.toAddCircle
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
n : ℕ
h :
  ∀ (θ : AddCircle (2 * π)),
    Eq (α := ℂ)
      ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (HPow.hPow (α := ℂ[X]) X n) : C(AddCircle (2 * π), ℂ)) :
            (a : AddCircle (2 * π)) → ℂ)
          θ :
        ℂ)
      ((fourier (↑n : ℤ) : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)
⊢ Eq (α := C(AddCircle (2 * π), ℂ))
    ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (HPow.hPow (α := ℂ[X]) X n) : C(AddCircle (2 * π), ℂ))
    (fourier (↑n : ℤ) : C(AddCircle (2 * π), ℂ))

Tactic:
ext θ
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
n : ℕ
θ : AddCircle (2 * π)
⊢ Eq (α := ℂ)
    ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (HPow.hPow (α := ℂ[X]) X n) : C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        θ :
      ℂ)
    ((fourier (↑n : ℤ) : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)

Tactic:
simp [toAddCircle, AddCircle.toCircle_nsmul]

Premises used: Polynomial.toAddCircle, AddCircle.toCircle_nsmul
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
n : ℕ
c : ℂ
h :
  ∀ (θ : AddCircle (2 * π)),
    Eq (α := ℂ)
      ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial n : (a : ℂ) → ℂ[X]) c) :
              C(AddCircle (2 * π), ℂ)) :
            (a : AddCircle (2 * π)) → ℂ)
          θ :
        ℂ)
      ((HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier (↑n : ℤ)) : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)
⊢ (toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial n : (a : ℂ) → ℂ[X]) c) =
    HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier (↑n : ℤ))

Tactic:
ext θ
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
n : ℕ
c : ℂ
θ : AddCircle (2 * π)
⊢ Eq (α := ℂ)
    ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial n : (a : ℂ) → ℂ[X]) c) :
            C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        θ :
      ℂ)
    ((HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier (↑n : ℤ)) : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)

Tactic:
simp [toAddCircle, AddCircle.toCircle_nsmul]

Premises used: Polynomial.toAddCircle, AddCircle.toCircle_nsmul
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
n : ℤ
⊢ n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)

Tactic:
have : n < 0 ∨ ∃ k : ℕ, n = k := lt_or_ge n 0 |>.imp_right Int.eq_ofNat_of_zero_le
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p_1 : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)
p q : ℂ[X]
hp :
  fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n =
    if 0 ≤ n then p.coeff n.natAbs else 0
hq :
  fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) q : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n =
    if 0 ≤ n then q.coeff n.natAbs else 0
add :
  ∀ (hn : n < 0),
    fourierCoeff (T := 2 * π)
        (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (p + q) : C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        n =
      if 0 ≤ n then (p + q).coeff n.natAbs else 0
add₁ :
  ∀ (k : ℕ)
    (hp :
      fourierCoeff (T := 2 * π)
          (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
            (a : AddCircle (2 * π)) → ℂ)
          (↑k : ℤ) =
        if LE.le (α := ℤ) 0 (↑k : ℤ) then p.coeff (Int.natAbs (↑k : ℤ)) else 0)
    (hq :
      fourierCoeff (T := 2 * π)
          (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) q : C(AddCircle (2 * π), ℂ)) :
            (a : AddCircle (2 * π)) → ℂ)
          (↑k : ℤ) =
        if LE.le (α := ℤ) 0 (↑k : ℤ) then q.coeff (Int.natAbs (↑k : ℤ)) else 0),
    fourierCoeff (T := 2 * π)
        (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (p + q) : C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        (↑k : ℤ) =
      if LE.le (α := ℤ) 0 (↑k : ℤ) then (p + q).coeff (Int.natAbs (↑k : ℤ)) else 0
⊢ fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (p + q) : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n =
    if 0 ≤ n then (p + q).coeff n.natAbs else 0

Tactic:
obtain (hn | ⟨k, rfl⟩) := this

Premises used: rfl
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p_1 : ℂ[X]
n : ℤ
p q : ℂ[X]
hp :
  fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n =
    if 0 ≤ n then p.coeff n.natAbs else 0
hq :
  fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) q : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n =
    if 0 ≤ n then q.coeff n.natAbs else 0
hn : n < 0
⊢ fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (p + q) : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n =
    if 0 ≤ n then (p + q).coeff n.natAbs else 0

Tactic:
simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]

Premises used: Polynomial.toAddCircle.integrable, fourierCoeff.add, not_le_of_gt
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p_1 p q : ℂ[X]
k : ℕ
hp :
  fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      (↑k : ℤ) =
    if LE.le (α := ℤ) 0 (↑k : ℤ) then p.coeff (Int.natAbs (↑k : ℤ)) else 0
hq :
  fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) q : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      (↑k : ℤ) =
    if LE.le (α := ℤ) 0 (↑k : ℤ) then q.coeff (Int.natAbs (↑k : ℤ)) else 0
⊢ fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (p + q) : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      (↑k : ℤ) =
    if LE.le (α := ℤ) 0 (↑k : ℤ) then (p + q).coeff (Int.natAbs (↑k : ℤ)) else 0

Tactic:
simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]

Premises used: Polynomial.toAddCircle.integrable, fourierCoeff.add, not_le_of_gt
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)
m : ℕ
a : ℂ
monomial :
  ∀ (hn : n < 0),
    Eq (α := ℂ)
      (fourierCoeff (T := 2 * π)
        (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) :
              C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        n)
      (if 0 ≤ n then coeff ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) n.natAbs else 0)
monomial₁ :
  ∀ (k : ℕ),
    Eq (α := ℂ)
      (fourierCoeff (T := 2 * π)
        (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) :
              C(AddCircle (2 * π), ℂ)) :
          (a : AddCircle (2 * π)) → ℂ)
        (↑k : ℤ))
      (if LE.le (α := ℤ) 0 (↑k : ℤ) then coeff ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) (Int.natAbs (↑k : ℤ))
      else 0)
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n)
    (if 0 ≤ n then coeff ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) n.natAbs else 0)

Tactic:
obtain (hn | ⟨k, rfl⟩) := this

Premises used: rfl
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
n : ℤ
m : ℕ
a : ℂ
hn : n < 0
monomial : n = (↑m : ℤ) → a = 0
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n)
    (if 0 ≤ n then coeff ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) n.natAbs else 0)

Tactic:
simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]

Premises used: Pi.single_apply, fourierCoeff.const_smul, Polynomial.coeff_monomial, Polynomial.toAddCircle_monomial_eq_smul_fourier, not_le_of_gt, fourierCoeff_fourier
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
n : ℤ
m : ℕ
a : ℂ
hn : n < 0
⊢ n = (↑m : ℤ) → a = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
m : ℕ
a : ℂ
k : ℕ
monomial : (if k = m then a else 0) = if m = k then a else 0
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      (↑k : ℤ))
    (if LE.le (α := ℤ) 0 (↑k : ℤ) then coeff ((Polynomial.monomial m : (a : ℂ) → ℂ[X]) a) (Int.natAbs (↑k : ℤ)) else 0)

Tactic:
simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]

Premises used: Pi.single_apply, fourierCoeff.const_smul, Polynomial.coeff_monomial, Polynomial.toAddCircle_monomial_eq_smul_fourier, not_le_of_gt, fourierCoeff_fourier
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
m : ℕ
a : ℂ
k : ℕ
⊢ (if k = m then a else 0) = if m = k then a else 0

Tactic:
grind
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
n : ℕ
⊢ fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      (↑n : ℤ) =
    p.coeff n

Tactic:
simp [fourierCoeff_toAddCircle]

Premises used: Polynomial.fourierCoeff_toAddCircle
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
n : ℤ
hn : n < 0
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n)
    0

Tactic:
simp [fourierCoeff_toAddCircle, hn]

Premises used: Polynomial.fourierCoeff_toAddCircle
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
⊢ Eq (α := ℝ)
    (∑' (i : ℤ),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          (fourierCoeff (T := 2 * π)
            (↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            i))
        2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)

Tactic:
have := tsum_sq_fourierCoeff (T := 2 * π) (p.toAddCircle.toLp 2 haarAddCircle ℂ)
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ)
    (∑' (i : ℤ),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          (fourierCoeff (T := 2 * π)
            (↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            i))
        2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
⊢ Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)

Tactic:
simp_rw [fourierCoeff_toLp, fourierCoeff_toAddCircle] at this

Premises used: fourierCoeff_toLp, Polynomial.fourierCoeff_toAddCircle
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
rw :
  ∀
    (this :
      Eq (α := ℝ)
        (∑ b ∈ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support,
          HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2)
        (∫ (t : AddCircle (2 * π)),
          HPow.hPow (β := ℕ)
            (norm (E := ℂ)
              ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                          ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                      AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
                  AddCircle (2 * π) → ℂ)
                t))
            2 ∂haarAddCircle)),
    Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
      (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
rw₁ :
  ∀ (b : ℤ) (hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support),
    HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
⊢ Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)

Tactic:
rw [tsum_eq_sum (s := p.support.map ⟨_, Nat.cast_injective⟩) (fun b hb => ?eq_zero)] at this

Premises used: tsum_eq_sum
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
inl : ∀ (h : 0 ≤ b), HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
inr : ∀ (h : b < 0), HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
⊢ HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0

Tactic:
obtain h | h := le_or_gt 0 b

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : 0 ≤ b
⊢ 0 ≤ b

Tactic:
h