awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : n ≠ 1
rw : Eq.{u + 1} (α := R) (if 1 = n then 1 else 0) 0
⊢ Eq.{u + 1} (α := R) (coeff X n) 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_X, if_neg hn.symm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
⊢ n ∈ p.support ↔ p.coeff n ≠ 0
have rcases : ∀ (toFinsupp : R[ℕ]), n ∈ { toFinsupp := toFinsupp : R[X] }.support ↔ { toFinsupp := toFinsupp : R[X] }.coeff n ≠ 0
Tactic: rcases p with ⟨⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
⊢ coeff ((C : (a : R) → R[X]) a) n = if n = 0 then a else 0
have h : n = 0 ↔ 0 = n
Tactic: convert! coeff_monomial (a := a) (m := n) (n := 0) using 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
h : n ≠ 0
⊢ Eq.{u + 1} (α := R) (coeff ((C : (a : R) → R[X]) a) n) 0
have rw : (if n = 0 then a else 0) = 0
Tactic: rw [coeff_C, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
h : n ≠ 0
rw : (if n = 0 then a else 0) = 0
⊢ Eq.{u + 1} (α := R) (coeff ((C : (a : R) → R[X]) a) n) 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_C, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a n : ℕ
h : a.AtLeastTwo
⊢ Eq.{u + 1} (α := R) (coeff (OfNat.ofNat a) (n + 1)) 0
have rw : Eq.{u + 1} (α := R) (coeff (↑(OfNat.ofNat a) : R[X]) (n + 1)) 0
Tactic: rw [← Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
  (monomial (n + 1) : (a : R) → R[X]) a
Tactic: rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
    (monomial (n + 1) : (a : R) → R[X]) a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a
have rw₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) * X =
  (monomial (n + 1) : (a : R) → R[X]) a
Tactic: rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) * X =
    (monomial (n + 1) : (a : R) → R[X]) a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a
have rw₂ : HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) a
Tactic: rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) * X =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₂ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a
have rw₃ : HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
  (monomial (n + 1) : (a : R) → R[X]) a
Tactic: rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) * X =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₂ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) a
rw₃ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
    (monomial (n + 1) : (a : R) → R[X]) a
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a
have rw₄ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) (a * 1) : R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X])
Tactic: rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n * X) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₁ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) * X =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₂ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) X = (monomial (n + 1) : (a : R) → R[X]) a
rw₃ :
  HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial 1 : (a : R) → R[X]) 1 : R[X]) =
    (monomial (n + 1) : (a : R) → R[X]) a
rw₄ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) (a * 1) : R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    (monomial (n + 1) : (a : R) → R[X]) a
have rw₅ : Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X]) ((monomial (n + 1) : (a : R) → R[X]) a : R[X])
Tactic: rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).toFinsupp = single n a
have rw : Eq (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) a)) (single n a)
Tactic: rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw : Eq (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) a)) (single n a)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).toFinsupp = single n a
have rw₁ : Eq (α := R[ℕ]) (single n a) (single n a)
Tactic: rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X = (monomial 1 : (a : R) → R[X]) a
have rw : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)
Tactic: rw [← C_mul_X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X = (monomial 1 : (a : R) → R[X]) a
have rw₁ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X
Tactic: rw [← C_mul_X_pow_eq_monomial, pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).toFinsupp = single 1 a
have rw : Eq (α := R[ℕ]) (toFinsupp ((monomial 1 : (a : R) → R[X]) a)) (single 1 a)
Tactic: rw [C_mul_X_eq_monomial, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R
rw : Eq (α := R[ℕ]) (toFinsupp ((monomial 1 : (a : R) → R[X]) a)) (single 1 a)
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).toFinsupp = single 1 a
have rw₁ : Eq (α := R[ℕ]) (single 1 a) (single 1 a)
Tactic: rw [C_mul_X_eq_monomial, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
have rcases : ∀ (f : ℕ →₀ R), { toFinsupp := f : R[X] } = q ↔ ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = q.coeff n
Tactic: rcases p with ⟨f : ℕ →₀ R⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
q : R[X]
f : ℕ →₀ R
⊢ { toFinsupp := f : R[X] } = q ↔ ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = q.coeff n
have rcases : ∀ (g : ℕ →₀ R),
  { toFinsupp := f : R[X] } = { toFinsupp := g } ↔
    ∀ (n : ℕ), { toFinsupp := f : R[X] }.coeff n = { toFinsupp := g : R[X] }.coeff n
Tactic: rcases q with ⟨g : ℕ →₀ R⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := AddSubmonoid R[X])
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a}) ⊤
have h : LE.le.{u} (α := AddSubmonoid R[X]) ⊤
  (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
Tactic: apply top_unique
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
⊢ LE.le.{u} (α := AddSubmonoid R[X]) ⊤
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
have h : LE.le (α := AddSubmonoid R[X])
  (AddSubmonoid.closure
    (Set.image (α := R[ℕ]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
      {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}))
  (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
Tactic: rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ←
    Finsupp.add_closure_setOf_eq_single, AddMonoidHom.map_mclosure]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
⊢ LE.le (α := AddSubmonoid R[X])
    (AddSubmonoid.closure
      (Set.image (α := R[ℕ]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
        {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}))
    (AddSubmonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
have h : Subset (α := Set R[ℕ]) {f : ℕ →₀ R | ∃ (a : ℕ) (b : R), f = Finsupp.single a b}
  (Set.preimage (β := R[X]) (⇑(RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R))) : (a : R[ℕ]) → R[X])
    {p : R[X] | ∃ (n : ℕ) (a : R), p = (monomial n : (a : R) → R[X]) a})
Tactic: refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
h : Eq.{u + 1} (α := R) 0 1
p : R[X]
⊢ p = 0
have rw : HSMul.hSMul (α := R) 1 p = 0
Tactic: rw [← one_smul R p, ← h, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
h : Eq.{u + 1} (α := R) 0 1
p : R[X]
rw : HSMul.hSMul (α := R) 1 p = 0
⊢ p = 0
have rw₁ : HSMul.hSMul (α := R) 0 p = 0
Tactic: rw [← one_smul R p, ← h, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
h : Eq.{u + 1} (α := R) 0 1
p : R[X]
rw : HSMul.hSMul (α := R) 1 p = 0
rw₁ : HSMul.hSMul (α := R) 0 p = 0
⊢ p = 0
have rw₂ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [← one_smul R p, ← h, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
c : R
h : c ≠ 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X).support = {1}
have rw : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) c) = {1}
Tactic: rw [C_mul_X_eq_monomial, support_monomial 1 h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
c : R
h : c ≠ 0
rw : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) c) = {1}
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X).support = {1}
have rw₁ : Eq (α := Finset ℕ) {1} {1}
Tactic: rw [C_mul_X_eq_monomial, support_monomial 1 h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
h : c ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)).support = {n}
have rw : support.{u} (R := R) ((monomial n : (a : R) → R[X]) c) = {n}
Tactic: rw [C_mul_X_pow_eq_monomial, support_monomial n h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
h : c ≠ 0
rw : support.{u} (R := R) ((monomial n : (a : R) → R[X]) c) = {n}
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)).support = {n}
have rw₁ : Eq (α := Finset ℕ) {n} {n}
Tactic: rw [C_mul_X_pow_eq_monomial, support_monomial n h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).toFinsupp = single n 1
have rw : Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) 1)) (single n 1)
Tactic: rw [X_pow_eq_monomial, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
rw : Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) 1)) (single n 1)
⊢ (HPow.hPow (α := R[X]) X n).toFinsupp = single n 1
have rw₁ : Eq.{u + 1} (α := R[ℕ]) (single n 1) (single n 1)
Tactic: rw [X_pow_eq_monomial, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
⊢ a • HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
have rw : HSMul.hSMul (β := R[X]) a ((monomial n : (a : R) → R[X]) 1) = (monomial n : (a : R) → R[X]) a
Tactic: rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw : HSMul.hSMul (β := R[X]) a ((monomial n : (a : R) → R[X]) 1) = (monomial n : (a : R) → R[X]) a
⊢ a • HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
have rw₁ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X])
  ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw : HSMul.hSMul (β := R[X]) a ((monomial n : (a : R) → R[X]) 1) = (monomial n : (a : R) → R[X]) a
rw₁ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
⊢ a • HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
have rw₂ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * 1) : R[X]) ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
rw : HSMul.hSMul (β := R[X]) a ((monomial n : (a : R) → R[X]) 1) = (monomial n : (a : R) → R[X]) a
rw₁ :
  Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (HSMul.hSMul (β := R) a 1) : R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
rw₂ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) (a * 1) : R[X]) ((monomial n : (a : R) → R[X]) a : R[X])
⊢ a • HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) a
have rw₃ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).support = {n}
have h : HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) 1
Tactic: convert! support_monomial n H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : Eq.{u + 1} (α := R) 1 0
⊢ support.{u} (R := R) X = ∅
have rw : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 1) = ∅
Tactic: rw [X, H, monomial_zero_right, support_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : Eq.{u + 1} (α := R) 1 0
rw : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 1) = ∅
⊢ support.{u} (R := R) X = ∅
have rw₁ : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 0) = ∅
Tactic: rw [X, H, monomial_zero_right, support_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : Eq.{u + 1} (α := R) 1 0
rw : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 1) = ∅
rw₁ : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 0) = ∅
⊢ support.{u} (R := R) X = ∅
have rw₂ : support.{u} (R := R) 0 = ∅
Tactic: rw [X, H, monomial_zero_right, support_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : Eq.{u + 1} (α := R) 1 0
rw : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 1) = ∅
rw₁ : support.{u} (R := R) ((monomial 1 : (a : R) → R[X]) 0) = ∅
rw₂ : support.{u} (R := R) 0 = ∅
⊢ support.{u} (R := R) X = ∅
have rw₃ : Eq (α := Finset ℕ) ∅ ∅
Tactic: rw [X, H, monomial_zero_right, support_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
⊢ support.{u} (R := R) X = {1}
have rw : (HPow.hPow (α := R[X]) (β := ℕ) X 1).support = {1}
Tactic: rw [← pow_one X, support_X_pow H 1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
rw : (HPow.hPow (α := R[X]) (β := ℕ) X 1).support = {1}
⊢ support.{u} (R := R) X = {1}
have rw₁ : Eq (α := Finset ℕ) {1} {1}
Tactic: rw [← pow_one X, support_X_pow H 1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X l) =
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) u : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) v : R[X]) (HPow.hPow (α := R[X]) X n) ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
have simp_rw : HAdd.hAdd (α := R[ℕ]) (single k u) (single l v) = HAdd.hAdd (α := R[ℕ]) (single m u) (single n v) ↔
  k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
Tactic: simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p * q = ∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) ↦ (monomial (i + j) : (a : R) → R[X]) (p.coeff i * a)
have a : (p * q).toFinsupp =
  toFinsupp (∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) ↦ (monomial (i + j) : (a : R) → R[X]) (p.coeff i * a))
Tactic: apply toFinsupp_injective
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (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 * 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))
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))
⊢ (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 * 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)))
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)))
⊢ (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 * 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)))
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)))
⊢ (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 * 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]