awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a :
  (p * q).toFinsupp =
    toFinsupp (∑ x ∈ p.support, ∑ x_1 ∈ q.support, (monomial (x + x_1) : (a : R) → R[X]) (p.coeff x * q.coeff x_1))
a₁ :
  (p * q).toFinsupp =
    toFinsupp
      (∑ x ∈ p.support,
        ∑ x_1 ∈ q.support,
          (monomial (x + x_1) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) x_1 : R)))
a₂ :
  (p * q).toFinsupp =
    ∑ x ∈ p.support,
      ∑ i ∈ q.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
a₃ :
  (p * q).toFinsupp =
    ∑ x ∈ p.toFinsupp.support,
      ∑ i ∈ q.toFinsupp.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
⊢ (p * q).toFinsupp =
    toFinsupp (∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) ↦ (monomial (i + j) : (a : R) → R[X]) (p.coeff i * a))
have a₄ : p.toFinsupp * q.toFinsupp =
  ∑ x ∈ p.toFinsupp.support,
    ∑ i ∈ q.toFinsupp.support,
      toFinsupp
        ((monomial (x + i) : (a : R) → R[X])
          (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
Tactic: simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial,
    AddMonoidAlgebra.mul_def, Finsupp.sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a :
  (p * q).toFinsupp =
    toFinsupp (∑ x ∈ p.support, ∑ x_1 ∈ q.support, (monomial (x + x_1) : (a : R) → R[X]) (p.coeff x * q.coeff x_1))
a₁ :
  (p * q).toFinsupp =
    toFinsupp
      (∑ x ∈ p.support,
        ∑ x_1 ∈ q.support,
          (monomial (x + x_1) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) x_1 : R)))
a₂ :
  (p * q).toFinsupp =
    ∑ x ∈ p.support,
      ∑ i ∈ q.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
a₃ :
  (p * q).toFinsupp =
    ∑ x ∈ p.toFinsupp.support,
      ∑ i ∈ q.toFinsupp.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
a₄ :
  p.toFinsupp * q.toFinsupp =
    ∑ x ∈ p.toFinsupp.support,
      ∑ i ∈ q.toFinsupp.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
⊢ (p * q).toFinsupp =
    toFinsupp (∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) ↦ (monomial (i + j) : (a : R) → R[X]) (p.coeff i * a))
have a₅ : p.toFinsupp * q.toFinsupp =
  ∑ x ∈ p.toFinsupp.support,
    ∑ x_1 ∈ q.toFinsupp.support,
      single (x + x_1)
        (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) x_1 : R))
Tactic: simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial,
    AddMonoidAlgebra.mul_def, Finsupp.sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a :
  (p * q).toFinsupp =
    toFinsupp (∑ x ∈ p.support, ∑ x_1 ∈ q.support, (monomial (x + x_1) : (a : R) → R[X]) (p.coeff x * q.coeff x_1))
a₁ :
  (p * q).toFinsupp =
    toFinsupp
      (∑ x ∈ p.support,
        ∑ x_1 ∈ q.support,
          (monomial (x + x_1) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) x_1 : R)))
a₂ :
  (p * q).toFinsupp =
    ∑ x ∈ p.support,
      ∑ i ∈ q.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
a₃ :
  (p * q).toFinsupp =
    ∑ x ∈ p.toFinsupp.support,
      ∑ i ∈ q.toFinsupp.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
a₄ :
  p.toFinsupp * q.toFinsupp =
    ∑ x ∈ p.toFinsupp.support,
      ∑ i ∈ q.toFinsupp.support,
        toFinsupp
          ((monomial (x + i) : (a : R) → R[X])
            (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) i : R)))
a₅ :
  p.toFinsupp * q.toFinsupp =
    ∑ x ∈ p.toFinsupp.support,
      ∑ x_1 ∈ q.toFinsupp.support,
        single (x + x_1)
          (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) x_1 : R))
⊢ (p * q).toFinsupp =
    toFinsupp (∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) ↦ (monomial (i + j) : (a : R) → R[X]) (p.coeff i * a))
have a₆ : Eq (α := R[ℕ])
  (Finsupp.sum p.toFinsupp fun (m₁ : ℕ) (r₁ : R) ↦
    Finsupp.sum q.toFinsupp fun (m₂ : ℕ) (r₂ : R) ↦ single (m₁ + m₂) (r₁ * r₂))
  (∑ x ∈ p.toFinsupp.support,
    ∑ x_1 ∈ q.toFinsupp.support,
      single (x + x_1)
        (HMul.hMul (α := R) (β := R) ((p.toFinsupp : (a : ℕ) → R) x : R) ((q.toFinsupp : (a : ℕ) → R) x_1 : R)))
Tactic: simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial,
    AddMonoidAlgebra.mul_def, Finsupp.sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ (p + q).sum f = p.sum f + q.sum f
have rw : { toFinsupp := p.toFinsupp + q.toFinsupp : R[X] }.sum f = p.sum f + q.sum f
Tactic: rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) = p
have simp_rw : (p.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) = p
Tactic: simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
a : R
⊢ motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0))
have zero : motive ((Polynomial.C : (a : R) → R[X]) a)
Tactic: rw [pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
n : ℕ
a : R
⊢ motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
have zero : motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0))
Tactic: induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
n : ℕ
a : R
zero : motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0))
⊢ motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
have succ : ∀ (n : ℕ) (ih : motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))),
  motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
Tactic: induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ motive p
have have : ∀
  (A :
    ∀ {n : ℕ} {a : R},
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))),
  motive p
Tactic: have A : ∀ {n : ℕ} {a}, motive (Polynomial.C a * X ^ n) := by
    intro n a
    induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have empty : motive (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: apply Finset.induction
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
empty :
  motive
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have insert : ∀ (a : ℕ) (s : Finset ℕ),
  a ∉ s →
    motive
        (∑ n ∈ s,
          HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive
        (∑ n ∈ insert a s,
          HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: apply Finset.induction
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive
    (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have h : Eq.{u + 1} (α := R[X])
  (∑ n ∈ ∅, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
  ((Polynomial.C : (a : R) → R[X]) 0)
Tactic: convert! C 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
n : ℕ
s : Finset ℕ
ns : n ∉ s
ih :
  motive
    (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive
    (∑ n ∈ insert n s,
      HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have insert : motive
  (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) +
    ∑ x ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
Tactic: rw [sum_insert ns]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive p
have B : ∀ (s : Finset ℕ),
  motive
    (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: have B : ∀ s : Finset ℕ, motive (s.sum fun n : ℕ => Polynomial.C (p.coeff n) * X ^ n) := by
    apply Finset.induction
    · convert! C 0
      exact C_0.symm
    · intro n s ns ih
      rw [sum_insert ns]
      exact add _ _ A ih
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
C : ∀ (a : R), motive ((Polynomial.C : (a : R) → R[X]) a)
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) →
      motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
A :
  ∀ {n : ℕ} {a : R},
    motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
B :
  ∀ (s : Finset ℕ),
    motive
      (∑ n ∈ s, HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive p
have rw : motive
  (∑ n ∈ p.support,
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) (p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
motive : R[X] → Prop
p : R[X]
add : ∀ (p q : R[X]), motive p → motive q → motive (p + q)
monomial : ∀ (n : ℕ) (a : R), motive ((Polynomial.monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
_h : motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
have rw : motive ((Polynomial.monomial (n + 1) : (a : R) → R[X]) a)
Tactic: rw [C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (HAdd.hAdd (α := R[X]) ((monomial n : (a : R) → R[X]) (p.coeff n) : R[X]) (erase n p)).toFinsupp = p.toFinsupp
have rw : HAdd.hAdd (α := R[ℕ]) (single n ((p.toFinsupp : (a : ℕ) → R) n) : R[ℕ]) (AddMonoidAlgebra.erase n p.toFinsupp) =
  p.toFinsupp
Tactic: rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n i : ℕ
⊢ (erase n p).coeff i = if i = n then 0 else p.coeff i
have rcases : ∀ (toFinsupp : R[ℕ]),
  (erase n { toFinsupp := toFinsupp : R[X] }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp : R[X] }.coeff i
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n i : ℕ
toFinsupp : R[ℕ]
⊢ (erase n { toFinsupp := toFinsupp : R[X] }).coeff i = if i = n then 0 else { toFinsupp := toFinsupp : R[X] }.coeff i
have simp : Eq (α := R) ((AddMonoidAlgebra.erase n toFinsupp : (a : ℕ) → R) i : R)
  (if i = n then 0 else (toFinsupp : (a : ℕ) → R) i : R)
Tactic: simp only [erase_def, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a
have h : ∀ (x : ℕ), (p.update n a).coeff x = Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
⊢ (p.update n a).coeff i = if i = n then a else p.coeff i
have rw : Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a i = if i = n then a else p.coeff i
Tactic: rw [coeff_update, Function.update_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
rw : Function.update (β := fun (a : ℕ) ↦ R) p.coeff n a i = if i = n then a else p.coeff i
⊢ (p.update n a).coeff i = if i = n then a else p.coeff i
have rw₁ : (if i = n then a else p.coeff i) = if i = n then a else p.coeff i
Tactic: rw [coeff_update, Function.update_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).coeff n = a
have rw : (if n = n then a else p.coeff n) = a
Tactic: rw [p.coeff_update_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (if n = n then a else p.coeff n) = a
⊢ (p.update n a).coeff n = a
have rw₁ : a = a
Tactic: rw [p.coeff_update_apply, if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
h : i ≠ n
⊢ (p.update n a).coeff i = p.coeff i
have rw : (if i = n then a else p.coeff i) = p.coeff i
Tactic: rw [p.coeff_update_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
i : ℕ
h : i ≠ n
rw : (if i = n then a else p.coeff i) = p.coeff i
⊢ (p.update n a).coeff i = p.coeff i
have rw₁ : p.coeff i = p.coeff i
Tactic: rw [p.coeff_update_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ p.update n 0 = erase n p
have a : ∀ (n_1 : ℕ), (p.update n 0).coeff n_1 = (erase n p).coeff n_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
⊢ (p.update n 0).coeff n_1 = (erase n p).coeff n_1
have a : (if n_1 = n then 0 else p.coeff n_1) = (erase n p).coeff n_1
Tactic: rw [coeff_update_apply, coeff_erase]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n n_1 : ℕ
a : (if n_1 = n then 0 else p.coeff n_1) = (erase n p).coeff n_1
⊢ (p.update n 0).coeff n_1 = (erase n p).coeff n_1
have a₁ : (if n_1 = n then 0 else p.coeff n_1) = if n_1 = n then 0 else p.coeff n_1
Tactic: rw [coeff_update_apply, coeff_erase]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
have simp : (if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support) =
  if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support
Tactic: simp only [support, update, Finsupp.support_update, AddMonoidAlgebra.update, ofCoeff,
      AddMonoidAlgebra.coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
inst_1 : Decidable (a = 0)
⊢ (p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
have simp : (if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support) =
  if a = 0 then p.toFinsupp.support.erase n else insert n p.toFinsupp.support
Tactic: classical
    simp only [support, update, Finsupp.support_update, AddMonoidAlgebra.update, ofCoeff,
      AddMonoidAlgebra.coeff]
    congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p.update n 0).support = p.support.erase n
have rw : (erase n p).support = p.support.erase n
Tactic: rw [update_zero_eq_erase, support_erase]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
rw : (erase n p).support = p.support.erase n
⊢ (p.update n 0).support = p.support.erase n
have rw₁ : p.support.erase n = p.support.erase n
Tactic: rw [update_zero_eq_erase, support_erase]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support
have rw : (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
Tactic: rw [support_update, if_neg ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
rw : (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
⊢ (p.update n a).support = insert n p.support
have rw₁ : insert n p.support = insert n p.support
Tactic: rw [support_update, if_neg ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support
have classical : (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
Tactic: classical rw [support_update, if_neg ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
classical : (if a = 0 then p.support.erase n else insert n p.support) = insert n p.support
⊢ (p.update n a).support = insert n p.support
have classical₁ : insert n p.support = insert n p.support
Tactic: classical rw [support_update, if_neg ha]