awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a b : R[X]
⊢ a.toFinsupp = b.toFinsupp ↔ a = b

Tactic:
toFinsupp_injective.eq_iff

Premises used: Polynomial.toFinsupp_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[X]
rw : a.toFinsupp = toFinsupp 0 ↔ a = 0
rw₁ rw₂ : a = 0 ↔ a = 0
⊢ a.toFinsupp = 0 ↔ a = 0

Tactic:
rw [← toFinsupp_zero, toFinsupp_inj]

Premises used: Polynomial.toFinsupp_inj, Polynomial.toFinsupp_zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[X]
rw : a.toFinsupp = toFinsupp 1 ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ a.toFinsupp = 1 ↔ a = 1

Tactic:
rw [← toFinsupp_one, toFinsupp_inj]

Premises used: Polynomial.toFinsupp_inj, Polynomial.toFinsupp_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a b : R[ℕ]
⊢ { toFinsupp := a : R[X] } = { toFinsupp := b } ↔ a = b

Tactic:
iff_of_eq (ofFinsupp.injEq _ _)

Premises used: Polynomial.ofFinsupp.injEq, iff_of_eq
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
rw : { toFinsupp := a : R[X] } = { toFinsupp := 0 } ↔ a = 0
rw₁ rw₂ : a = 0 ↔ a = 0
⊢ { toFinsupp := a : R[X] } = 0 ↔ a = 0

Tactic:
rw [← ofFinsupp_zero, ofFinsupp_inj]

Premises used: Polynomial.ofFinsupp_zero, Polynomial.ofFinsupp_inj
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
rw : { toFinsupp := a : R[X] } = { toFinsupp := 1 } ↔ a = 1
rw₁ rw₂ : a = 1 ↔ a = 1
⊢ { toFinsupp := a : R[X] } = 1 ↔ a = 1

Tactic:
rw [← ofFinsupp_one, ofFinsupp_inj]

Premises used: Polynomial.ofFinsupp_inj, Polynomial.ofFinsupp_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) { toFinsupp := (↑n : R[ℕ]) } (↑n : R[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp (↑n : R[X])) (↑n : R[ℕ])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R[X]) { toFinsupp := OfNat.ofNat n } (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : FaithfulSMul S R
_s₁ _s₂ : S
h : ∀ (a : R[X]), _s₁ • a = _s₂ • a
apply : ∀ (a : ℕ →₀ R), _s₁ • a = _s₂ • a
⊢ _s₁ = _s₂

Tactic:
apply eq_of_smul_eq_smul (α := ℕ →₀ R)

Premises used: FaithfulSMul.eq_of_smul_eq_smul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a_1 b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : FaithfulSMul S R
_s₁ _s₂ : S
h : ∀ (a : R[X]), _s₁ • a = _s₂ • a
a : ℕ →₀ R
⊢ _s₁ • a = _s₂ • a

Tactic:
congr_arg toFinsupp (h ⟨a⟩)

Premises used: Polynomial.toFinsupp, congr_arg, AddMonoidAlgebra, Polynomial.ofFinsupp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a_1 b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : FaithfulSMul S R
_s₁ _s₂ : S
h : ∀ (a : R[X]), _s₁ • a = _s₂ • a
a : ℕ →₀ R
⊢ _s₁ • a = _s₂ • a

Tactic:
exact congr_arg toFinsupp (h ⟨a⟩)

Premises used: Polynomial.toFinsupp, congr_arg, Polynomial.ofFinsupp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m_1 n_1 : ℕ
inst : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst_1 : SMulZeroClass S₁ R
inst_2 : SMulZeroClass S₂ R
inst_3 : SMulCommClass S₁ S₂ R
m : S₁
n : S₂
f : R[ℕ]
simp_rw : { toFinsupp := m • n • f : R[X] } = { toFinsupp := n • m • f }
⊢ m • n • { toFinsupp := f : R[X] } = n • m • { toFinsupp := f : R[X] }

Tactic:
simp_rw [← ofFinsupp_smul, smul_comm m n f]

Premises used: Polynomial.ofFinsupp_smul, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst_1 : SMul S₁ S₂
inst_2 : SMulZeroClass S₁ R
inst_3 : SMulZeroClass S₂ R
inst_4 : IsScalarTower S₁ S₂ R
x : S₁
y : S₂
toFinsupp : R[ℕ]
simp_rw : { toFinsupp := (x • y) • toFinsupp : R[X] } = { toFinsupp := x • y • toFinsupp }
⊢ (x • y) • { toFinsupp := toFinsupp : R[X] } = x • y • { toFinsupp := toFinsupp : R[X] }

Tactic:
simp_rw [← ofFinsupp_smul, smul_assoc]

Premises used: smul_assoc, Polynomial.ofFinsupp_smul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst_1 : Semiring K
inst_2 : DistribSMul α K
inst_3 : IsScalarTower α K K
x : α
toFinsupp toFinsupp_1 : K[ℕ]
simp_rw :
  x • { toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
simp_rw₁ :
  { toFinsupp := x • toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
simp_rw₂ : { toFinsupp := x • toFinsupp * toFinsupp_1 : K[X] } = x • { toFinsupp := toFinsupp * toFinsupp_1 : K[X] }
simp_rw₃ : { toFinsupp := x • toFinsupp * toFinsupp_1 : K[X] } = { toFinsupp := x • (toFinsupp * toFinsupp_1) }
⊢ (x • { toFinsupp := toFinsupp : K[X] }) • { toFinsupp := toFinsupp_1 : K[X] } =
    x • { toFinsupp := toFinsupp : K[X] } • { toFinsupp := toFinsupp_1 : K[X] }

Tactic:
simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]

Premises used: smul_mul_assoc, Polynomial.ofFinsupp_smul, Polynomial.ofFinsupp_mul, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : SMulZeroClass.{u_1, u} Sᵐᵒᵖ R
inst_3 : IsCentralScalar S R
m_1 : S
toFinsupp : R[ℕ]
simp_rw : { toFinsupp := MulOpposite.op m_1 • toFinsupp : R[X] } = { toFinsupp := m_1 • toFinsupp }
⊢ MulOpposite.op m_1 • { toFinsupp := toFinsupp : R[X] } = m_1 • { toFinsupp := toFinsupp : R[X] }

Tactic:
simp_rw [← ofFinsupp_smul, op_smul_eq_smul]

Premises used: Polynomial.ofFinsupp_smul, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Module S R
inst_3 : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : Eq.{u + 1} (α := R[X]) ((fun (x : R[X]) ↦ s • x) { toFinsupp := f }) ((fun (x : R[X]) ↦ s • x) { toFinsupp := g })
e_toFinsupp : f = g
⊢ { toFinsupp := f : R[X] } = { toFinsupp := g }

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Module S R
inst_3 : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : Eq.{u + 1} (α := R[X]) ((fun (x : R[X]) ↦ s • x) { toFinsupp := f }) ((fun (x : R[X]) ↦ s • x) { toFinsupp := g })
e_toFinsupp : Eq.{u + 1} (α := R[ℕ]) ((fun (x : R[ℕ]) ↦ s • x) f) ((fun (x : R[ℕ]) ↦ s • x) g)
⊢ f = g

Tactic:
apply hs.isSMulRegular

Premises used: IsRegular.isSMulRegular
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : Semiring S
inst_2 : Module S R
inst_3 : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : Eq.{u + 1} (α := R[X]) ((fun (x : R[X]) ↦ s • x) { toFinsupp := f }) ((fun (x : R[X]) ↦ s • x) { toFinsupp := g })
⊢ Eq.{u + 1} (α := R[ℕ]) ((fun (x : R[ℕ]) ↦ s • x) f) ((fun (x : R[ℕ]) ↦ s • x) g)

Tactic:
simpa using congr(($hfg).toFinsupp)
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
inst_1 : Subsingleton R
x : R[ℕ]
apply : x = 0
⊢ { toFinsupp := x : R[X] } = default

Tactic:
apply congr_arg ofFinsupp

Premises used: congr_arg, Polynomial.ofFinsupp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
inst_1 : Subsingleton R
x : R[ℕ]
⊢ x = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s : Finset ι
f : ι → R[ℕ]
⊢ Eq.{u + 1} (α := R[X]) { toFinsupp := ∑ i ∈ s, f i } (∑ i ∈ s, { toFinsupp := f i })

Tactic:
map_sum (toFinsuppIso R).symm f s

Premises used: map_sum, Polynomial.toFinsuppIso, RingEquiv.symm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s : Finset ι
f : ι → R[X]
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp (∑ i ∈ s, f i)) (∑ i ∈ s, (f i).toFinsupp)

Tactic:
map_sum (toFinsuppIso R) f s

Premises used: map_sum, Polynomial.toFinsuppIso
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[ℕ]
rw rw₁ : p.support = p.support
⊢ { toFinsupp := p : R[X] }.support = p.support

Tactic:
rw [support]

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw rw₁ : p.toFinsupp.support = p.toFinsupp.support
⊢ p.toFinsupp.support = p.support

Tactic:
rw [support]

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ support.{u} (R := R) 0 = ∅

Tactic:
rfl

Premises used: Polynomial.support, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
rcases : ∀ (toFinsupp : R[ℕ]), { toFinsupp := toFinsupp : R[X] }.support = ∅ ↔ { toFinsupp := toFinsupp : R[X] } = 0
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
toFinsupp : R[ℕ]
⊢ { toFinsupp := toFinsupp : R[X] }.support = ∅ ↔ { toFinsupp := toFinsupp : R[X] } = 0

Tactic:
simp [support]

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.support.Nonempty ↔ p ≠ 0

Tactic:
Finset.nonempty_iff_ne_empty.trans support_eq_empty.not

Premises used: Iff.not, Finset.nonempty_iff_ne_empty, Iff.trans, Polynomial.support_eq_empty
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ #p.support = 0 ↔ p = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n_1 : ℕ
inst : Semiring R
p q : R[X]
n : ℕ
x y : R
⊢ { toFinsupp := single n (x + y) } =
    HAdd.hAdd (α := R[X]) { toFinsupp := single n x : R[X] } { toFinsupp := single n y : R[X] }

Tactic:
simp [← ofFinsupp_add]

Premises used: Polynomial.ofFinsupp_add
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n_1 : ℕ
inst : Semiring R
p q : R[X]
n : ℕ
r x : R
⊢ { toFinsupp := single n (r • x) } =
    HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) r : R) { toFinsupp := single n x : R[X] }

Tactic:
simp [← ofFinsupp_smul]

Premises used: Polynomial.ofFinsupp_smul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
⊢ Eq (α := R[ℕ]) (toFinsupp ((monomial n : (a : R) → R[X]) r)) (single n r)

Tactic:
simp [monomial]

Premises used: Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
⊢ Eq (α := R[X]) { toFinsupp := single n r } ((monomial n : (a : R) → R[X]) r)

Tactic:
simp [monomial]

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

Tactic:
(monomial n).map_zero

Premises used: LinearMap.map_zero, Polynomial.monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) ((monomial 0 : (a : R) → R[X]) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n m : ℕ
r s : R
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) r : R[X])
        ((monomial m : (a : R) → R[X]) s : R[X])).toFinsupp =
    toFinsupp ((monomial (n + m) : (a : R) → R[X]) (r * s))

Tactic:
simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]

Premises used: Polynomial.toFinsupp_monomial, Polynomial.toFinsupp_mul, AddMonoidAlgebra.single_mul_single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
⊢ HPow.hPow (α := R[X]) (β := ℕ) ((monomial n : (a : R) → R[X]) r : R[X]) 0 =
    (monomial (n * 0) : (a : R) → R[X]) (HPow.hPow (β := ℕ) r 0)

Tactic:
simp [pow_zero, monomial_zero_one]

Premises used: Polynomial.monomial_zero_one, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
ih : HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = (monomial (n * k) : (a : R) → R[X]) (r ^ k)
⊢ HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (k + 1) =
    (monomial (n * (k + 1)) : (a : R) → R[X]) (r ^ (k + 1))

Tactic:
simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

Premises used: pow_succ, add_comm, mul_add, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
r : R
k : ℕ
zero :
  HPow.hPow (α := R[X]) (β := ℕ) ((monomial n : (a : R) → R[X]) r : R[X]) 0 =
    (monomial (n * 0) : (a : R) → R[X]) (HPow.hPow (β := ℕ) r 0)
succ :
  ∀ (k : ℕ)
    (ih :
      HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = (monomial (n * k) : (a : R) → R[X]) (r ^ k)),
    HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) (k + 1) =
      (monomial (n * (k + 1)) : (a : R) → R[X]) (r ^ (k + 1))
⊢ HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = (monomial (n * k) : (a : R) → R[X]) (r ^ k)

Tactic:
induction k with
  | zero => simp [pow_zero, monomial_zero_one]
  | succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

Premises used: pow_succ, Polynomial.monomial_zero_one, add_comm, pow_zero, AddMonoidAlgebra.zero, mul_add, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ HSMul.hSMul (β := R[X]) a ((monomial n : (a : R) → R[X]) b : R[X]) = (monomial n : (a : R) → R[X]) (a • b)

Tactic:
toFinsupp_injective <| AddMonoidAlgebra.smul_single _ _ _

Premises used: Polynomial.toFinsupp_injective, AddMonoidAlgebra.smul_single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Injective.{u + 1, u + 1} (α := R) (β := R[X]) (⇑(monomial n) : (a : R) → R[X])

Tactic:
(toFinsuppIso R).symm.injective.comp (single_injective n)

Premises used: Finsupp.single_injective, RingEquiv.injective, Function.Injective.comp, Polynomial.toFinsuppIso, RingEquiv.symm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
t : R
n : ℕ
⊢ Eq (α := R[X]) ((monomial n : (a : R) → R[X]) t : R[X]) (0 : R[X]) ↔ t = 0

Tactic:
LinearMap.map_eq_zero_iff _ (Polynomial.monomial_injective n)

Premises used: Polynomial.monomial_injective, LinearMap.map_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
m n : ℕ
a b : R
rw :
  Eq.{u + 1} (α := R[ℕ]) (toFinsupp ((monomial m : (a : R) → R[X]) a)) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0
rw₁ : Eq (α := R[ℕ]) (single m a) (toFinsupp ((monomial n : (a : R) → R[X]) b)) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
rw₂ : Eq (α := R[ℕ]) (single m a) (single n b) ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
rw₃ rw₄ : m = n ∧ a = b ∨ a = 0 ∧ b = 0 ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
⊢ Eq (α := R[X]) ((monomial m : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) ↔
    m = n ∧ a = b ∨ a = 0 ∧ b = 0

Tactic:
rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]

Premises used: Finsupp.single_eq_single_iff, Polynomial.toFinsupp_monomial, Polynomial.toFinsupp_inj
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
simpa [support] using Finsupp.support_add

Premises used: Finsupp.support_add, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
⊢ Eq.{u + 1} (α := R[X]) (AddHom.toFun (LinearMap.toAddHom (monomial 0)) 1) 1

Tactic:
simp [monomial_zero_one]

Premises used: Polynomial.monomial_zero_one
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
⊢ ∀ (x y : R),
    AddHom.toFun (LinearMap.toAddHom (monomial 0)) (x * y) =
      HMul.hMul (α := R[X]) (AddHom.toFun (LinearMap.toAddHom (monomial 0)) x)
        (AddHom.toFun (LinearMap.toAddHom (monomial 0)) y)

Tactic:
simp [monomial_mul_monomial]

Premises used: Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
⊢ Eq.{u + 1} (α := R[X]) (AddHom.toFun (LinearMap.toAddHom (monomial 0)) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
⊢ Eq (α := R[X]) ((monomial 0 : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) a : R[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R
⊢ Eq (α := R[ℕ]) (toFinsupp ((C : (a : R) → R[X]) a)) (single 0 a)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
inst : Semiring R
⊢ (C : (a : R) → R[X]) (a * b) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])

Tactic:
C.map_mul a b

Premises used: Polynomial.C, RingHom.map_mul
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
inst : Semiring R
⊢ (C : (a : R) → R[X]) (a + b) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X])

Tactic:
C.map_add a b

Premises used: Polynomial.C, RingHom.map_add
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
s : S
r : R
⊢ HSMul.hSMul (β := R[X]) s ((C : (a : R) → R[X]) r : R[X]) = (C : (a : R) → R[X]) (s • r)

Tactic:
smul_monomial _ _ r

Premises used: Polynomial.smul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
⊢ (C : (a : R) → R[X]) (a ^ n) = HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) n

Tactic:
C.map_pow a n

Premises used: Polynomial.C, RingHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) (↑n : R[X])

Tactic:
map_natCast C n

Premises used: Polynomial.C, map_natCast
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
n : ℕ
inst : Semiring R
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((monomial n : (a : R) → R[X]) b : R[X]) =
    (monomial n : (a : R) → R[X]) (a * b)

Tactic:
simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]

Premises used: zero_add, Polynomial.monomial_zero_left, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
a b : R
n : ℕ
inst : Semiring R
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    (monomial n : (a : R) → R[X]) (a * b)

Tactic:
simp only [← monomial_zero_left, monomial_mul_monomial, add_zero]

Premises used: Polynomial.monomial_zero_left, add_zero, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) ((monomial 1 : (a : R) → R[X]) 1) X

Tactic:
rfl

Premises used: Polynomial.X, rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ (monomial 0 : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) (β := ℕ) X 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n
succ : (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n * X
succ₁ : (monomial (n + 1) : (a : R) → R[X]) 1 = HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) X
succ₂ :
  (monomial (n + 1) : (a : R) → R[X]) 1 =
    HMul.hMul (α := R[X]) ((monomial n : (a : R) → R[X]) 1) ((monomial 1 : (a : R) → R[X]) 1)
succ₃ :
  Eq (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) 1 : R[X])
    ((monomial (n + 1) : (a : R) → R[X]) (HMul.hMul (α := R) 1 1) : R[X])
succ₄ succ₅ : Eq.{u + 1} (α := R[X]) ((monomial (n + 1) : (a : R) → R[X]) 1) ((monomial (n + 1) : (a : R) → R[X]) 1)
⊢ (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)

Tactic:
rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

Premises used: Polynomial.monomial_one_one_eq_X, pow_succ, mul_one, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
n : ℕ
zero : (monomial 0 : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) (β := ℕ) X 0
succ :
  ∀ (n : ℕ) (ih : (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n),
    (monomial (n + 1) : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X (n + 1)
⊢ (monomial n : (a : R) → R[X]) 1 = HPow.hPow (α := R[X]) X n

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

Premises used: Polynomial.monomial_one_one_eq_X, pow_succ, AddMonoidAlgebra.zero, mul_one, Polynomial.monomial_mul_monomial
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp X) (single 1 1)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
a : R
he : Eq.{u + 1} (α := R[X]) X ((C : (a : R) → R[X]) a)
⊢ False

Tactic:
simpa using monomial_eq_monomial_iff.1 he

Premises used: Polynomial.monomial_eq_monomial_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
rcases : ∀ (toFinsupp : R[ℕ]), X * { toFinsupp := toFinsupp : R[X] } = { toFinsupp := toFinsupp : R[X] } * X
⊢ X * p = p * X

Tactic:
rcases p with ⟨⟩
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
toFinsupp : R[ℕ]
simp : single 1 1 * toFinsupp = toFinsupp * single 1 1
⊢ X * { toFinsupp := toFinsupp : R[X] } = { toFinsupp := toFinsupp : R[X] } * X

Tactic:
simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, ofFinsupp.injEq]

Premises used: Polynomial.ofFinsupp_single, Polynomial.ofFinsupp_mul, Polynomial.ofFinsupp.injEq, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
toFinsupp : R[ℕ]
hfg :
  ∀ (m : ℕ), Eq (α := R) ((single 1 1 * toFinsupp : (a : ℕ) → R) m : R) ((toFinsupp * single 1 1 : (a : ℕ) → R) m : R)
⊢ single 1 1 * toFinsupp = toFinsupp * single 1 1

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
toFinsupp : R[ℕ]
m : ℕ
⊢ Eq (α := R) ((single 1 1 * toFinsupp : (a : ℕ) → R) m : R) ((toFinsupp * single 1 1 : (a : ℕ) → R) m : R)

Tactic:
simp [AddMonoidAlgebra.mul_apply, add_comm]

Premises used: AddMonoidAlgebra.mul_apply, add_comm
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ HPow.hPow (α := R[X]) (β := ℕ) X 0 * p = p * HPow.hPow (α := R[X]) (β := ℕ) X 0

Tactic:
simp