-- 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
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
⊢ 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 monomial : ∀ (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)
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