awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
M : Type u_1
inst_1 : AddZeroClass M
f g : AddMonoidHom.{u, u_1} R[X] M
h :
  ∀ (n : ℕ) (a : R),
    Eq.{u_1 + 1} (α := M) ((f : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)
      ((g : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)
n : ℕ
a : R
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)
    ((g : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)

Tactic:
h n a
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
M : Type u_1
inst_1 : AddZeroClass M
f g : AddMonoidHom.{u, u_1} R[X] M
h :
  ∀ (n : ℕ) (a : R),
    Eq.{u_1 + 1} (α := M) ((f : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)
      ((g : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)
n : ℕ
a : R
⊢ Eq.{u_1 + 1} (α := M) ((f : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)
    ((g : (a : R[X]) → M) ((monomial n : (a : R) → R[X]) a : R[X]) : M)

Tactic:
exact h n a
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
M : Type u_1
inst_1 : AddZeroClass M
f g : AddMonoidHom.{u, u_1} R[X] M
h : ∀ (n : ℕ), f.comp (LinearMap.toAddMonoidHom (monomial n)) = g.comp (LinearMap.toAddMonoidHom (monomial n))
⊢ f = g

Tactic:
addHom_ext fun n => DFunLike.congr_fun (h n)

Premises used: DFunLike.congr_fun, Polynomial.addHom_ext
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : R[X] →ₗ[R] M
h : ∀ (n : ℕ), f ∘ₗ monomial n = g ∘ₗ monomial n
⊢ f = g

Tactic:
LinearMap.toAddMonoidHom_injective <| addHom_ext fun n => LinearMap.congr_fun (h n)

Premises used: LinearMap.toAddMonoidHom_injective, Polynomial.addHom_ext, LinearMap.congr_fun
-- Module: Mathlib.Algebra.Polynomial.Basic
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
rw₂ rw₃ : Eq.{u + 1} (α := R[X]) 0 0
⊢ p = 0

Tactic:
rw [← one_smul R p, ← h, zero_smul]

Premises used: one_smul, zero_smul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
H : a ≠ 0
⊢ Finsupp.support (single n a) = {n}

Tactic:
Finsupp.support_single _ H

Premises used: Finsupp.support_single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
H : a ≠ 0
⊢ Finsupp.support (single n a) = {n}

Tactic:
exact Finsupp.support_single _ H

Premises used: Finsupp.support_single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ Finsupp.support (single n a) ⊆ {n}

Tactic:
Finsupp.support_single_subset

Premises used: Set.Mem, setOf, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ Finsupp.support (single n a) ⊆ {n}

Tactic:
exact Finsupp.support_single_subset

Premises used: Finsupp.support_single_subset
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
h : a ≠ 0
⊢ support.{u} (R := R) ((C : (a : R) → R[X]) a) = {0}

Tactic:
support_monomial 0 h

Premises used: Polynomial.support_monomial, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
⊢ support.{u} (R := R) ((C : (a : R) → R[X]) a) ⊆ {0}

Tactic:
support_monomial' 0 a

Premises used: Set.Mem, setOf, OfNat.ofNat, Polynomial.support_monomial'
-- Module: Mathlib.Algebra.Polynomial.Basic
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}
rw₁ rw₂ : Eq (α := Finset ℕ) {1} {1}
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X).support = {1}

Tactic:
rw [C_mul_X_eq_monomial, support_monomial 1 h]

Premises used: Polynomial.support_monomial, Polynomial.C_mul_X_eq_monomial, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
c : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) X).support ⊆ {1}

Tactic:
simpa only [C_mul_X_eq_monomial] using support_monomial' 1 c

Premises used: Polynomial.C_mul_X_eq_monomial, OfNat.ofNat, Polynomial.support_monomial'
-- Module: Mathlib.Algebra.Polynomial.Basic
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}
rw₁ rw₂ : Eq (α := Finset ℕ) {n} {n}
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)).support = {n}

Tactic:
rw [C_mul_X_pow_eq_monomial, support_monomial n h]

Premises used: Polynomial.support_monomial, Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
c : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X n)).support ⊆ {n}

Tactic:
simpa only [C_mul_X_pow_eq_monomial] using support_monomial' n c

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.support_monomial'
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
k m : ℕ
x y : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ⊆
    {k, m}

Tactic:
support_add.trans
    (union_subset
      ((support_C_mul_X_pow' k x).trans (singleton_subset_iff.mpr (mem_insert_self k {m})))
      ((support_C_mul_X_pow' m y).trans
        (singleton_subset_iff.mpr (mem_insert_of_mem (mem_singleton_self m)))))

Premises used: Iff.mpr, Finset.union_subset, Finset.mem_singleton_self, Finset.mem_insert_self, Finset.singleton_subset_iff, HasSubset.Subset.trans, Polynomial.support_C_mul_X_pow', Polynomial.support_add, Finset.mem_insert_of_mem, Singleton.singleton
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
x y z : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ⊆
    {k, m, n}

Tactic:
support_add.trans
    (union_subset
      (support_add.trans
        (union_subset
          ((support_C_mul_X_pow' k x).trans (singleton_subset_iff.mpr (mem_insert_self k {m, n})))
          ((support_C_mul_X_pow' m y).trans
            (singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_self m {n}))))))
      ((support_C_mul_X_pow' n z).trans
        (singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n))))))

Premises used: Iff.mpr, Finset.union_subset, Finset.mem_singleton_self, Finset.mem_insert_self, Finset.singleton_subset_iff, HasSubset.Subset.trans, Insert.insert, Polynomial.support_C_mul_X_pow', Polynomial.support_add, Finset.mem_insert_of_mem, Singleton.singleton
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) 1

Tactic:
(monomial_one_right_eq_X_pow n).symm

Premises used: Polynomial.monomial_one_right_eq_X_pow, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
rw : Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) 1)) (single n 1)
rw₁ rw₂ : Eq.{u + 1} (α := R[ℕ]) (single n 1) (single n 1)
⊢ (HPow.hPow (α := R[X]) X n).toFinsupp = single n 1

Tactic:
rw [X_pow_eq_monomial, toFinsupp_monomial]

Premises used: Polynomial.toFinsupp_monomial, Polynomial.X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
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])
rw₃ rw₄ : Eq (α := R[X]) ((monomial n : (a : R) → R[X]) a : 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

Tactic:
rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]

Premises used: Polynomial.X_pow_eq_monomial, Polynomial.smul_monomial, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
n : ℕ
⊢ support.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = {n}

Tactic:
support_monomial n H

Premises used: Polynomial.support_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
n : ℕ
h : HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) 1
⊢ (HPow.hPow (α := R[X]) X n).support = {n}

Tactic:
convert! support_monomial n H

Premises used: Polynomial.support_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
n : ℕ
⊢ HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) 1

Tactic:
X_pow_eq_monomial n

Premises used: Polynomial.X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
n : ℕ
⊢ HPow.hPow (α := R[X]) X n = (monomial n : (a : R) → R[X]) 1

Tactic:
exact X_pow_eq_monomial n

Premises used: Polynomial.X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
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 = ∅
rw₃ rw₄ : Eq (α := Finset ℕ) ∅ ∅
⊢ support.{u} (R := R) X = ∅

Tactic:
rw [X, H, monomial_zero_right, support_zero]

Premises used: Polynomial.monomial_zero_right, Polynomial.X, Polynomial.support_zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
H : ¬Eq.{u + 1} (α := R) 1 0
rw : (HPow.hPow (α := R[X]) (β := ℕ) X 1).support = {1}
rw₁ rw₂ : Eq (α := Finset ℕ) {1} {1}
⊢ support.{u} (R := R) X = {1}

Tactic:
rw [← pow_one X, support_X_pow H 1]

Premises used: pow_one, Polynomial.support_X_pow, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
ha : a ≠ 0
i j : ℕ
⊢ Eq (α := R[X]) ((monomial i : (a : R) → R[X]) a : R[X]) ((monomial j : (a : R) → R[X]) a : R[X]) ↔ i = j

Tactic:
simp only [← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]

Premises used: Polynomial.ofFinsupp_single, Finsupp.single_left_inj, Polynomial.ofFinsupp.injEq
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
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
⊢ 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

Tactic:
simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]

Premises used: Polynomial.toFinsupp_monomial, Polynomial.toFinsupp_inj, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.toFinsupp_add
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ 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:
Finsupp.single_add_single_eq_single_add_single hu hv

Premises used: Finsupp.single_add_single_eq_single_add_single, AddMonoidAlgebra
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ 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:
exact Finsupp.single_add_single_eq_single_add_single hu hv

Premises used: Finsupp.single_add_single_eq_single_add_single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
p : R[X]
⊢ (↑n : R[X]) * p = n • p

Tactic:
(nsmul_eq_mul _ _).symm

Premises used: nsmul_eq_mul, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
⊢ p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

Tactic:
rfl

Premises used: Polynomial.sum, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
p : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
s : Finset ℕ
hs : p.support ⊆ s
⊢ p.sum f = ∑ n ∈ s, f n (p.coeff n)

Tactic:
Finsupp.sum_of_support_subset _ hs f (fun i _ ↦ hf i)

Premises used: Polynomial.sum, Polynomial.coeff, Polynomial.support, Finsupp.sum_of_support_subset
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
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))
⊢ p * q = ∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) ↦ (monomial (i + j) : (a : R) → R[X]) (p.coeff i * a)

Tactic:
apply toFinsupp_injective

Premises used: Polynomial.toFinsupp_injective
-- Module: Mathlib.Algebra.Polynomial.Basic
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))
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)))
⊢ (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:
simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial,
    AddMonoidAlgebra.mul_def, Finsupp.sum]

Premises used: Polynomial.toFinsupp_monomial, Polynomial.sum, Finsupp.sum, AddMonoidAlgebra.mul_def, Polynomial.coeff, Polynomial.toFinsupp_mul, Polynomial.toFinsupp_sum, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0

Tactic:
simp [sum]

Premises used: Polynomial.sum
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
n : ℕ
a : R
f : ℕ → R → S
hf : f n 0 = 0
⊢ sum ((monomial n : (a : R) → R[X]) a) f = f n a

Tactic:
Finsupp.sum_single_index hf

Premises used: Finsupp.sum_single_index, Polynomial.sum, Polynomial.coeff, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
β : Type u_1
inst_1 : AddCommMonoid β
f : ℕ → R → β
h : f 0 0 = 0
⊢ sum ((C : (a : R) → R[X]) a) f = f 0 a

Tactic:
sum_monomial_index a f h

Premises used: Polynomial.sum_monomial_index
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
f : ℕ → R → S
hf : f 1 0 = 0
⊢ sum X f = f 1 1

Tactic:
sum_monomial_index 1 f hf

Premises used: Polynomial.sum_monomial_index, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Basic
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₂
rw : { toFinsupp := p.toFinsupp + q.toFinsupp : R[X] }.sum f = p.sum f + q.sum f
⊢ (p + q).sum f = p.sum f + q.sum f

Tactic:
rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from rfl]

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
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₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp : R[X] }.sum f = p.sum f + q.sum f

Tactic:
Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)

Premises used: Polynomial.sum, Polynomial.coeff, Finsupp.sum_add_index, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
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₂
⊢ { toFinsupp := p.toFinsupp + q.toFinsupp : R[X] }.sum f = p.sum f + q.sum f

Tactic:
exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ p.sum (f + g) = p.sum f + p.sum g

Tactic:
simp [sum_def, Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, Polynomial.sum_def
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ (p.sum fun (n : ℕ) (x : R) ↦ f n x + g n x) = p.sum f + p.sum g

Tactic:
sum_add' _ _ _

Premises used: Polynomial.sum_add'
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : AddCommMonoid S
p : R[X]
b : R
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
⊢ (b • p).sum f = p.sum fun (n : ℕ) (a : R) ↦ f n (b * a)

Tactic:
Finsupp.sum_smul_index hf

Premises used: Finsupp.sum_smul_index, Polynomial.sum, Polynomial.coeff, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
T : Type u_2
inst_1 : DistribSMul T R
inst_2 : AddCommMonoid S
p : R[X]
b : T
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
⊢ (b • p).sum f = p.sum fun (n : ℕ) (a : R) ↦ f n (b • a)

Tactic:
Finsupp.sum_smul_index' hf

Premises used: Finsupp.sum_smul_index', Polynomial.sum, Polynomial.coeff, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
T : Type u_2
inst_1 : AddCommMonoid S
inst_2 : DistribSMul T S
p : R[X]
b : T
f : ℕ → R → S
⊢ b • p.sum f = p.sum fun (n : ℕ) (a : R) ↦ b • f n a

Tactic:
Finsupp.smul_sum

Premises used: Polynomial.sum, Polynomial.coeff, Finsupp.smul_sum, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
simp_rw : (p.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a) = p
⊢ (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

Tactic:
simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.sum_monomial_eq
-- Module: Mathlib.Algebra.Polynomial.Basic
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
zero : motive ((Polynomial.C : (a : R) → R[X]) a)
⊢ motive (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 0))

Tactic:
rw [pow_zero, mul_one]

Premises used: pow_zero, mul_one
-- Module: Mathlib.Algebra.Polynomial.Basic
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 ((Polynomial.C : (a : R) → R[X]) a)

Tactic:
C a
-- Module: Mathlib.Algebra.Polynomial.Basic
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 ((Polynomial.C : (a : R) → R[X]) a)

Tactic:
exact C a
-- Module: Mathlib.Algebra.Polynomial.Basic
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
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:
monomial _ _ ih
-- Module: Mathlib.Algebra.Polynomial.Basic
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
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:
exact monomial _ _ ih