awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : 0 < m
hm₂ : m ≤ 2
h : P m
⊢ P 1 ∨ P 2
have 1 : ∀ (hm₀ : LT.lt (α := ℕ) 0 1) (hm₂ : LE.le (α := ℕ) 1 2) (h : P 1), P 1 ∨ P 2
Tactic: interval_cases m
Cleared hypotheses: hm₀, hm₂, h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : 0 < m
hm₂ : m ≤ 2
h : P m
1 : ∀ (hm₀ : LT.lt (α := ℕ) 0 1) (hm₂ : LE.le (α := ℕ) 1 2) (h : P 1), P 1 ∨ P 2
⊢ P 1 ∨ P 2
have 2 : ∀ (hm₀ : LT.lt (α := ℕ) 0 2) (hm₂ : LE.le (α := ℕ) 2 2) (h : P 2), P 1 ∨ P 2
Tactic: interval_cases m
Cleared hypotheses: hm₀, hm₂, h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : LT.lt (α := ℕ) 0 1
hm₂ : LE.le (α := ℕ) 1 2
h : P 1
⊢ P 1 ∨ P 2
have 1 : ¬P 1 → P 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
P : ℕ → Prop
m : ℕ
hm₀ : LT.lt (α := ℕ) 0 2
hm₂ : LE.le (α := ℕ) 2 2
h : P 2
⊢ P 1 ∨ P 2
have 2 : ¬P 1 → P 2
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 1)
f₁ : ℝ[X]
hm : f₁.Monic
hirr : Irreducible f₁
f₂ : ℝ[X]
hf₂ : f = f₁ * f₂
⊢ f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2
have help : ∀ {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m), P 1 ∨ P 2
Tactic: have help {P : ℕ → Prop} {m : ℕ} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m) : P 1 ∨ P 2 := by
    interval_cases m <;> tauto
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have inl : ∀ (g₁ g₂ : ℝ[X]) (h : f = g₁ * g₂) (hd₁ : g₁.IsMonicOfDegree 1),
  ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Tactic: obtain ⟨g₁, g₂, hd₁ | hd₂, h⟩ := hf.eq_isMonicOfDegree_one_or_two_mul
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
inl :
  ∀ (g₁ g₂ : ℝ[X]) (h : f = g₁ * g₂) (hd₁ : g₁.IsMonicOfDegree 1),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have inr : ∀ (g₁ g₂ : ℝ[X]) (h : f = g₁ * g₂) (hd₂ : g₁.IsMonicOfDegree 2),
  ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Tactic: obtain ⟨g₁, g₂, hd₁ | hd₂, h⟩ := hf.eq_isMonicOfDegree_one_or_two_mul
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hf₁ : (g₁ * g₂).IsMonicOfDegree (2 + n)
Tactic: rw [h, add_comm] at hf
Cleared hypotheses: hf, h, hd₁
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
Goal:
f : ℝ[X]
n : ℕ
hf : f.IsMonicOfDegree (n + 2)
g₁ g₂ : ℝ[X]
h : f = g₁ * g₂
hd₂ : g₁.IsMonicOfDegree 2
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hf₁ : (g₁ * g₂).IsMonicOfDegree (2 + n)
Tactic: rw [h, add_comm] at hf
Cleared hypotheses: hf, h, hd₂
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
Goal:
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hg₂ : g₂.IsMonicOfDegree (n + 1)
Tactic: have hg₂ := of_mul_left hd₁ <| (show 2 + n = 1 + (n + 1) by lia) ▸ hf
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
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)
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have inl : ∀ (p₁ p₂ : ℝ[X]) (h' : g₂ = p₁ * p₂) (hp₁ : p₁.IsMonicOfDegree 1),
  ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Tactic: obtain ⟨p₁, p₂, hp₁ | hp₂, h'⟩ := hg₂.eq_isMonicOfDegree_one_or_two_mul
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (goal)
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)
inl :
  ∀ (p₁ p₂ : ℝ[X]) (h' : g₂ = p₁ * p₂) (hp₁ : p₁.IsMonicOfDegree 1),
    ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have inl₁ : ∀ (p₁ p₂ : ℝ[X]) (h' : g₂ = p₁ * p₂) (hp₂ : p₁.IsMonicOfDegree 2),
  ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
Tactic: obtain ⟨p₁, p₂, hp₁ | hp₂, h'⟩ := hg₂.eq_isMonicOfDegree_one_or_two_mul
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
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
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hf₁ : (g₁ * p₁ * p₂).IsMonicOfDegree (2 + n)
Tactic: rw [h', ← mul_assoc] at h hf
Cleared hypotheses: hf, h, h', hp₁
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
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)
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have h₁ : f = g₁ * p₁ * p₂
Tactic: rw [h', ← mul_assoc] at h hf
Cleared hypotheses: hf, h, h', hp₁
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
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
⊢ ∃ (f₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have hf₁ : (p₁ * (g₁ * p₂)).IsMonicOfDegree (2 + n)
Tactic: rw [h', mul_left_comm] at h hf
Cleared hypotheses: hf, h, h', hp₂
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Factorization (hypothesis)
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₁ : ℝ[X]) (f₂ : ℝ[X]), f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
have h₁ : f = p₁ * (g₁ * p₂)
Tactic: rw [h', mul_left_comm] at h hf
Cleared hypotheses: hf, h, h', hp₂
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
c : ℂ
⊢ (toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((C : (a : ℂ) → ℂ[X]) c) =
    HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier 0)
have 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 * π)) → ℂ) θ : ℂ)
Tactic: ext θ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
⊢ Eq (α := C(AddCircle (2 * π), ℂ)) ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) X : C(AddCircle (2 * π), ℂ))
    (fourier 1 : C(AddCircle (2 * π), ℂ))
have h : ∀ (θ : AddCircle (2 * π)),
  Eq (α := ℂ)
    ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) X : C(AddCircle (2 * π), ℂ)) : (a : AddCircle (2 * π)) → ℂ)
        θ :
      ℂ)
    ((fourier 1 : (a : AddCircle (2 * π)) → ℂ) θ : ℂ)
Tactic: ext θ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
n : ℕ
⊢ Eq (α := C(AddCircle (2 * π), ℂ))
    ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) (HPow.hPow (α := ℂ[X]) X n) : C(AddCircle (2 * π), ℂ))
    (fourier (↑n : ℤ) : C(AddCircle (2 * π), ℂ))
have 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 * π)) → ℂ) θ : ℂ)
Tactic: ext θ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
n : ℕ
c : ℂ
⊢ (toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial n : (a : ℂ) → ℂ[X]) c) =
    HSMul.hSMul (β := C(AddCircle (2 * π), ℂ)) c (fourier (↑n : ℤ))
have 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 * π)) → ℂ) θ : ℂ)
Tactic: ext θ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (hypothesis)
Goal:
p : ℂ[X]
n : ℤ
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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
⊢ 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
have 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
Tactic: obtain (hn | ⟨k, rfl⟩) := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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
⊢ 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
have 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
Tactic: obtain (hn | ⟨k, rfl⟩) := this
Cleared hypotheses: n, this, hp, hq
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
p : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)
m : ℕ
a : ℂ
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n)
    (if 0 ≤ n then coeff ((monomial m : (a : ℂ) → ℂ[X]) a) n.natAbs else 0)
have monomial : ∀ (hn : n < 0),
  Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n)
    (if 0 ≤ n then coeff ((monomial m : (a : ℂ) → ℂ[X]) a) n.natAbs else 0)
Tactic: obtain (hn | ⟨k, rfl⟩) := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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)
⊢ 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)
have 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)
Tactic: obtain (hn | ⟨k, rfl⟩) := this
Cleared hypotheses: n, this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
p : ℂ[X]
n : ℤ
m : ℕ
a : ℂ
hn : n < 0
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      n)
    (if 0 ≤ n then coeff ((monomial m : (a : ℂ) → ℂ[X]) a) n.natAbs else 0)
have monomial : n = (↑m : ℤ) → a = 0
Tactic: simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
p : ℂ[X]
m : ℕ
a : ℂ
k : ℕ
⊢ Eq (α := ℂ)
    (fourierCoeff (T := 2 * π)
      (⇑((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) ((monomial m : (a : ℂ) → ℂ[X]) a) :
            C(AddCircle (2 * π), ℂ)) :
        (a : AddCircle (2 * π)) → ℂ)
      (↑k : ℤ))
    (if LE.le (α := ℤ) 0 (↑k : ℤ) then coeff ((monomial m : (a : ℂ) → ℂ[X]) a) (Int.natAbs (↑k : ℤ)) else 0)
have monomial : (if k = m then a else 0) = if m = k then a else 0
Tactic: simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
p : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)
⊢ 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
have add : ∀ (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),
  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: induction p using Polynomial.induction_on' with obtain (hn | ⟨k, rfl⟩) := this
  | add p q hp hq =>
    simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]
  | monomial m a =>
    simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
p : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)
add :
  ∀ (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),
    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
⊢ 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
have add₁ : ∀ (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: induction p using Polynomial.induction_on' with obtain (hn | ⟨k, rfl⟩) := this
  | add p q hp hq =>
    simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]
  | monomial m a =>
    simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
Goal:
p : ℂ[X]
n : ℤ
this : n < 0 ∨ ∃ (k : ℕ), n = (↑k : ℤ)
add :
  ∀ (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),
    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₁ :
  ∀ (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
⊢ 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
have add₂ : ∀ (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: induction p using Polynomial.induction_on' with obtain (hn | ⟨k, rfl⟩) := this
  | add p q hp hq =>
    simp_all [not_le_of_gt, fourierCoeff.add (toAddCircle.integrable p) (toAddCircle.integrable q)]
  | monomial m a =>
    simp_all [not_le_of_gt, coeff_monomial, toAddCircle_monomial_eq_smul_fourier,
      fourierCoeff.const_smul, fourierCoeff_fourier, Pi.single_apply]
    grind
Cleared hypotheses: n, this