awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
apply_fun : (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum
inj : Function.Injective (α := AddMonoidAlgebra M ι) AddMonoidAlgebra.toDirectSum
⊢ (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra

Tactic:
apply_fun AddMonoidAlgebra.toDirectSum

Premises used: AddMonoidAlgebra.toDirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum

Tactic:
simp
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
inj : Function.LeftInverse (α := AddMonoidAlgebra M ι) toAddMonoidAlgebra AddMonoidAlgebra.toDirectSum
inj₁ : (⨁ (x : ι), M) → AddMonoidAlgebra M ι
⊢ Function.Injective (α := AddMonoidAlgebra M ι) AddMonoidAlgebra.toDirectSum

Tactic:
apply Function.LeftInverse.injective

Premises used: Function.LeftInverse.injective
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f : M[ι]
n : ℕ
⊢ (f ^ n).toDirectSum = f.toDirectSum ^ n

Tactic:
map_pow addMonoidAlgebraRingEquivDirectSum f n

Premises used: Finsupp.toDFinsupp, addMonoidAlgebraRingEquivDirectSum, map_pow, AddMonoidAlgebra.toDirectSum
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f : M[ι]
n : ℕ
⊢ (f ^ n).toDirectSum = f.toDirectSum ^ n

Tactic:
exact map_pow addMonoidAlgebraRingEquivDirectSum f n

Premises used: addMonoidAlgebraRingEquivDirectSum, map_pow
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
f : M[ι]
n : ℕ
⊢ (f ^ n).toDirectSum = f.toDirectSum ^ n

Tactic:
classical exact map_pow addMonoidAlgebraRingEquivDirectSum f n

Premises used: addMonoidAlgebraRingEquivDirectSum, map_pow
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
n : ℕ
⊢ (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n

Tactic:
map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

Premises used: addMonoidAlgebraRingEquivDirectSum, map_pow, DirectSum.toAddMonoidAlgebra, DFinsupp.toFinsupp, RingEquiv.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
n : ℕ
⊢ (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n

Tactic:
exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

Premises used: addMonoidAlgebraRingEquivDirectSum, map_pow, RingEquiv.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : Semiring M
inst_3 : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
n : ℕ
⊢ (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n

Tactic:
classical exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

Premises used: addMonoidAlgebraRingEquivDirectSum, map_pow, RingEquiv.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) 1 ((monomial 0 : (a : R) → MvPolynomial σ R) 1)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ →₀ ℕ
a : R
⊢ Eq (α := Finsupp.{u_1, u} (σ →₀ ℕ) R) (Finsupp.single s a) ((monomial s : (a : R) → MvPolynomial σ R) a)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
⊢ p * q =
    sum p fun (m : σ →₀ ℕ) (a : R) ↦
      sum q fun (n : σ →₀ ℕ) (b : R) ↦ (monomial (m + n) : (a : R) → MvPolynomial σ R) (a * b)

Tactic:
AddMonoidAlgebra.mul_def ..

Premises used: AddMonoidAlgebra.mul_def, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := R →+* MvPolynomial σ R) (algebraMap R (MvPolynomial σ R)) C

Tactic:
rfl

Premises used: MvPolynomial.C, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
r : R
⊢ Eq (α := MvPolynomial σ S₁) ((algebraMap R (MvPolynomial σ S₁) : (a : R) → MvPolynomial σ S₁) r : MvPolynomial σ S₁)
    ((C : (a : S₁) → MvPolynomial σ S₁) ((algebraMap R S₁ : (a : R) → S₁) r) : MvPolynomial σ S₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
r : R
hr : r ≠ 0
⊢ Injective (β := MvPolynomial σ R) fun (s : σ →₀ ℕ) ↦ (monomial s : (a : R) → MvPolynomial σ R) r

Tactic:
Finsupp.single_left_injective hr

Premises used: Finsupp.single_left_injective, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s t : σ →₀ ℕ
r : R
hr : r ≠ 0
⊢ Eq (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial t : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    s = t

Tactic:
Finsupp.single_left_inj hr

Premises used: Finsupp.single_left_inj, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) 0) 0

Tactic:
map_zero _

Premises used: map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) 1) 1

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst : CommSemiring R
⊢ HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
    AddMonoidAlgebra.single (0 + s) (a * a')

Tactic:
have := single_mul_single 0 s a a'
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst : CommSemiring R
this :
  HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
    AddMonoidAlgebra.single (0 + s) (a * a')
⊢ HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
    AddMonoidAlgebra.single s (a * a')

Tactic:
rw [zero_add] at this

Premises used: zero_add
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst : CommSemiring R
this :
  HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
    AddMonoidAlgebra.single s (a * a')
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R) =
    (monomial s : (a : R) → MvPolynomial σ R) (a * a')

Tactic:
this

Premises used: Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a a' : R
s : σ →₀ ℕ
inst : CommSemiring R
this :
  HMul.hMul (α := AddMonoidAlgebra.{u, u_1} R (σ →₀ ℕ)) (AddMonoidAlgebra.single 0 a) (AddMonoidAlgebra.single s a') =
    AddMonoidAlgebra.single s (a * a')
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R) =
    (monomial s : (a : R) → MvPolynomial σ R) (a * a')

Tactic:
exact this
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a a' : R
inst : CommSemiring R
⊢ (C : (a : R) → MvPolynomial σ R) (a + a') =
    HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R)

Tactic:
Finsupp.single_add _ _ _

Premises used: Finsupp.single_add, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a a' : R
inst : CommSemiring R
⊢ (C : (a : R) → MvPolynomial σ R) (a * a') =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a' : MvPolynomial σ R)

Tactic:
C_mul_monomial.symm

Premises used: MvPolynomial.C_mul_monomial, Eq.symm, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
a : R
n : ℕ
⊢ (C : (a : R) → MvPolynomial σ R) (a ^ n) =
    HPow.hPow (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) n

Tactic:
map_pow _ _ _

Premises used: map_pow
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
σ : Type u_2
R : Type u_3
inst : CommSemiring R
⊢ Injective (α := R) (β := MvPolynomial σ R) (⇑C : (a : R) → MvPolynomial σ R)

Tactic:
Finsupp.single_injective _

Premises used: Finsupp.single_injective, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : IsEmpty σ
⊢ Surjective (α := R) (β := MvPolynomial σ R) (⇑C : (a : R) → MvPolynomial σ R)

Tactic:
fun p => ⟨p.toFun 0, Finsupp.ext fun a => ?_⟩

Premises used: Finsupp.toFun, Finsupp.ext, Exists.intro, OfNat.ofNat, Function.Surjective
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : IsEmpty σ
refine :
  ∀ (p : MvPolynomial σ R) (a : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((((C : (a : R) → MvPolynomial σ R) (p.toFun 0) : MvPolynomial σ R) : (a : σ →₀ ℕ) → R) a : R)
      ((p : (a : σ →₀ ℕ) → R) a : R)
⊢ Surjective (α := R) (β := MvPolynomial σ R) (⇑C : (a : R) → MvPolynomial σ R)

Tactic:
refine fun p => ⟨p.toFun 0, Finsupp.ext fun a => ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
simp : p.toFun 0 = (p : (a : σ →₀ ℕ) → R) 0
⊢ Eq.{u_2 + 1} (α := R) ((((C : (a : R) → MvPolynomial σ R) (p.toFun 0) : MvPolynomial σ R) : (a : σ →₀ ℕ) → R) a : R)
    ((p : (a : σ →₀ ℕ) → R) a : R)

Tactic:
simp only [C_apply, ← single_eq_monomial, (Finsupp.ext isEmptyElim (α := σ) : a = 0),
    single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.ext, isEmptyElim, MvPolynomial.C_apply, MvPolynomial.single_eq_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : IsEmpty σ
p : MvPolynomial σ R
a : σ →₀ ℕ
⊢ p.toFun 0 = (p : (a : σ →₀ ℕ) → R) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
σ : Type u_2
R : Type u_3
inst : CommSemiring R
r s : R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) ↔
    r = s

Tactic:
(C_injective σ R).eq_iff

Premises used: Function.Injective.eq_iff, MvPolynomial.C_injective
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
rw :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) 0 : MvPolynomial σ R) ↔
    a = 0
rw₁ rw₂ : a = 0 ↔ a = 0
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (0 : MvPolynomial σ R) ↔ a = 0

Tactic:
rw [← map_zero C, C_inj]

Premises used: map_zero, MvPolynomial.C_inj, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
⊢ Ne (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (0 : MvPolynomial σ R) ↔ a ≠ 0

Tactic:
C_eq_zero.ne

Premises used: MvPolynomial.C_eq_zero, Iff.ne
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n m : σ_1
s : σ_1 →₀ ℕ
inst : CommSemiring R_1
inst_1 : CommSemiring S₁
p q : MvPolynomial σ_1 R_1
σ : Type u_2
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Nontrivial R
⊢ Nontrivial (MvPolynomial σ R)

Tactic:
inferInstanceAs (Nontrivial <| AddMonoidAlgebra R (σ →₀ ℕ))

Premises used: _private.0.MvPolynomial.nontrivial_of_nontrivial._proof_1
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n m : σ_1
s : σ_1 →₀ ℕ
inst : CommSemiring R_1
inst_1 : CommSemiring S₁
p q : MvPolynomial σ_1 R_1
σ : Type u_2
R : Type u_3
inst_2 : CommSemiring R
inst_3 : Infinite R
⊢ Infinite (MvPolynomial σ R)

Tactic:
Infinite.of_injective C (C_injective _ _)

Premises used: Infinite.of_injective, MvPolynomial.C_injective, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R_1 : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R_1
e : ℕ
n m : σ_1
s : σ_1 →₀ ℕ
inst : CommSemiring R_1
inst_1 : CommSemiring S₁
p q : MvPolynomial σ_1 R_1
σ : Type u_2
R : Type u_3
inst_2 : Nonempty σ
inst_3 : CommSemiring R
inst_4 : Nontrivial R
⊢ Infinite (MvPolynomial σ R)

Tactic:
Infinite.of_injective ((fun s : σ →₀ ℕ => monomial s 1) ∘ Finsupp.single (Classical.arbitrary σ))
    <| (monomial_left_injective one_ne_zero).comp (Finsupp.single_injective _)

Premises used: Finsupp.single_injective, Infinite.of_injective, MvPolynomial.monomial, Function.comp, MvPolynomial.monomial_left_injective, Function.Injective.comp, Classical.arbitrary, one_ne_zero, OfNat.ofNat, DFunLike.coe, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
inst_2 : NoZeroDivisors R
⊢ NoZeroDivisors (MvPolynomial σ R)

Tactic:
inferInstanceAs (NoZeroDivisors (AddMonoidAlgebra ..))

Premises used: _private.0.MvPolynomial.instNoZeroDivisors._proof_1
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
inst_2 : IsCancelAdd R
inst_3 : IsCancelMulZero R
⊢ IsCancelMulZero (MvPolynomial σ R)

Tactic:
inferInstanceAs (IsCancelMulZero (AddMonoidAlgebra ..))

Premises used: _private.0.MvPolynomial.instIsCancelMulZeroOfIsCancelAdd._proof_1
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
zero : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑0 : R)) (↑0 : MvPolynomial σ R)
succ :
  ∀ (n : ℕ),
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) (↑n : MvPolynomial σ R) →
      Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑(n + 1) : R)) (↑(n + 1) : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) (↑n : MvPolynomial σ R)

Tactic:
induction n
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑0 : R)) (↑0 : MvPolynomial σ R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
h : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) (↑n : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑(n + 1) : R)) (↑(n + 1) : MvPolynomial σ R)

Tactic:
simp [*]
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
p : MvPolynomial σ R
⊢ HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p = a • p

Tactic:
(Algebra.smul_def a p).symm

Premises used: Algebra.smul_def, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
a : R
⊢ a • p = HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) p

Tactic:
C_mul'.symm

Premises used: MvPolynomial.C_mul', Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
inst : CommSemiring R
rw :
  (C : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (1 : MvPolynomial σ R)
rw₁ rw₂ :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ (C : (a : R) → MvPolynomial σ R) a = HSMul.hSMul (β := MvPolynomial σ R) a 1

Tactic:
rw [← C_mul', mul_one]

Premises used: MvPolynomial.C_mul', mul_one
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
S₁ : Type u_2
inst_1 : SMulZeroClass S₁ R
r : S₁
⊢ HSMul.hSMul (β := MvPolynomial σ R) r ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) =
    (monomial s : (a : R) → MvPolynomial σ R) (r • a)

Tactic:
Finsupp.smul_single _ _ _

Premises used: AddMonoidAlgebra, Finsupp.smul_single, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Injective (α := σ) (β := MvPolynomial σ R) X

Tactic:
(monomial_left_injective one_ne_zero).comp (Finsupp.single_left_injective one_ne_zero)

Premises used: MvPolynomial.X, Finsupp.single_left_injective, MvPolynomial.monomial_left_injective, Function.Injective.comp, one_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
m n : σ
⊢ Eq (α := MvPolynomial σ R) (X m) (X n) ↔ m = n

Tactic:
X_injective.eq_iff

Premises used: MvPolynomial.X_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ HPow.hPow (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) e =
    (monomial (e • s) : (a : R) → MvPolynomial σ R) (a ^ e)

Tactic:
AddMonoidAlgebra.single_pow ..

Premises used: AddMonoidAlgebra.single_pow, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s s' : σ →₀ ℕ
a b : R
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial s' : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) =
    (monomial (s + s') : (a : R) → MvPolynomial σ R) (a * b)

Tactic:
AddMonoidAlgebra.single_mul_single ..

Premises used: AddMonoidAlgebra.single_mul_single, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R)
    ((monomialOneHom R σ : (a : Multiplicative (σ →₀ ℕ)) → MvPolynomial σ R) s : MvPolynomial σ R)
    ((monomial s : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
e : ℕ
n : σ
inst : CommSemiring R
⊢ HPow.hPow (α := MvPolynomial σ R) (X n) e = (monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1

Tactic:
simp [X, monomial_pow]

Premises used: MvPolynomial.X, MvPolynomial.monomial_pow
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
rw :
  (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R) ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
rw₂ rw₃ :
  Eq (α := MvPolynomial σ R) ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ (monomial (s + Finsupp.single n e) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X n) e)

Tactic:
rw [X_pow_eq_monomial, monomial_mul, mul_one]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.monomial_mul, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
a : R
e : ℕ
n : σ
s : σ →₀ ℕ
inst : CommSemiring R
rw :
  (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial (Finsupp.single n e) : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R) ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) (1 * a) : MvPolynomial σ R)
rw₂ rw₃ :
  Eq (α := MvPolynomial σ R) ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ (monomial (Finsupp.single n e + s) : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (β := MvPolynomial σ R) (HPow.hPow (α := MvPolynomial σ R) (X n) e)
      ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
rw [X_pow_eq_monomial, monomial_mul, one_mul]

Premises used: MvPolynomial.X_pow_eq_monomial, MvPolynomial.monomial_mul, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Basic
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
s : σ
a : R
n : ℕ
rw :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (HAdd.hAdd (α := σ →₀ ℕ) 0 (Finsupp.single s n)) : (a : R) → MvPolynomial σ R) a
rw₁ :
  HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n)
rw₂ rw₃ :
  HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    HMul.hMul (α := MvPolynomial σ R) ((monomial 0 : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n)
⊢ HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (X s) n) =
    (monomial (Finsupp.single s n) : (a : R) → MvPolynomial σ R) a

Tactic:
rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]

Premises used: MvPolynomial.C_apply, MvPolynomial.monomial_add_single, zero_add, Finsupp.single