awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ Eq (α := A[X]) ((monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) 1 : A)) : A[X])
    ((monomial n : (a : A) → A[X]) a : A[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ Eq (α := A[X]) ((monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) 0 : A)) : A[X])
    (0 : A[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p : A[X]
⊢ (polyEquivTensor R A : (a : A[X]) → A ⊗[R] R[X]) p = eval₂ (↑includeLeft : A →+* A ⊗[R] R[X]) (1 ⊗ₜ[R] X) p

Tactic:
rfl

Premises used: PolyEquivTensor.invFun, rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ (AlgEquiv.symm (polyEquivTensor R A) : (a : A ⊗[R] R[X]) → A[X]) (a ⊗ₜ[R] p) =
    HSMul.hSMul (β := A[X]) a (Polynomial.map (algebraMap R A) p)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, List.foldl, RingHomClass.toRingHom, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ Eq.{u_3 + 1} (α := A[X]) ((AlgEquiv.symm (polyEquivTensor R A) : (a : A ⊗[R] R[X]) → A[X]) (a ⊗ₜ[R] p) : A[X])
    (p.sum fun (n : ℕ) (r : R) ↦
        (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) r : A)) :
      A[X])

Tactic:
toFunAlgHom_apply_tmul _ _ _ _

Premises used: Quotient.liftOn', PolyEquivTensor.toFunAlgHom_apply_tmul, AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A_1 : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A_1
inst_3 : Algebra R A_1
inst_4 : Algebra R S
inst_5 : Algebra S A_1
inst_6 : IsScalarTower R S A_1
A : Type u_4
inst_7 : CommSemiring A
inst_8 : Algebra R A
a : A
⊢ Eq (α := A ⊗[R] R[X]) (Equiv.toFun (AlgEquiv.toEquiv (polyEquivTensor R A)) ((algebraMap A A[X] : (a : A) → A[X]) a))
    ((algebraMap A (A ⊗[R] R[X]) : (a : A) → A ⊗[R] R[X]) a)

Tactic:
simp
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := (a : A[X]) → A ⊗[R] R[X]) (⇑(polyEquivTensor' R A) : (a : A[X]) → A ⊗[R] R[X])
    (⇑(polyEquivTensor R A) : (a : A[X]) → A ⊗[R] R[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
⊢ Eq (α := (a : A ⊗[R] R[X]) → A[X]) (⇑(AlgEquiv.symm (polyEquivTensor' R A)) : (a : A ⊗[R] R[X]) → A[X])
    (⇑(AlgEquiv.symm (polyEquivTensor R A)) : (a : A ⊗[R] R[X]) → A[X])

Tactic:
rfl

Premises used: Equiv.symm, rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
x : R[X]
x_1 : A[X]
a :
  ∀ (n : ℕ),
    (HMul.hMul (α := A[X]) (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
            x_1).coeff
        n =
      (HMul.hMul (β := A[X]) x_1
            (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])).coeff
        n
⊢ HMul.hMul (α := A[X]) (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
      x_1 =
    HMul.hMul (β := A[X]) x_1
      (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
x : R[X]
x_1 : A[X]
n : ℕ
a :
  Eq.{u_3 + 1} (α := A)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      coeff (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x) p.swap.1 *
        x_1.coeff p.swap.2)
    (∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      x_1.coeff x_2.1 *
        coeff (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x) x_2.2)
⊢ (HMul.hMul (α := A[X]) (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
          x_1).coeff
      n =
    (HMul.hMul (β := A[X]) x_1
          (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])).coeff
      n

Tactic:
rw [coeff_mul, ← Finset.Nat.sum_antidiagonal_swap, coeff_mul]

Premises used: Polynomial.coeff_mul, Finset.Nat.sum_antidiagonal_swap
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
x : R[X]
x_1 : A[X]
n : ℕ
⊢ Eq.{u_3 + 1} (α := A)
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      coeff (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x) p.swap.1 *
        x_1.coeff p.swap.2)
    (∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      x_1.coeff x_2.1 *
        coeff (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x) x_2.2)

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
⊢ Eq (α := RingHom.{u_1, u_3} R[X] A[X]) (algebraMap R[X] A[X]) (mapRingHom (algebraMap R A))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
⊢ IsScalarTower.{u_1, u_2, u_3} R S[X] A[X]

Tactic:
have : IsScalarTower S S[X] A[X] := .of_algebraMap_eq' (mapRingHom_comp_C _).symm
  .to₁₃₄ _ S _ _

Premises used: Algebra.algebraMap, IsScalarTower.to₁₃₄, IsScalarTower.of_algebraMap_eq', Polynomial, Polynomial.mapRingHom_comp_C, Eq.symm
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
⊢ IsScalarTower.{u_1, u_2, u_3} R[X] S[X] A[X]

Tactic:
.of_algebraMap_eq' <|
  congr(mapRingHom $(IsScalarTower.algebraMap_eq R S A)).trans (mapRingHom_comp ..).symm

Premises used: congrArg, id, IsScalarTower.of_algebraMap_eq', Polynomial.mapRingHom, IsScalarTower.algebraMap_eq, Polynomial.mapRingHom_comp, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : FaithfulSMul R A
⊢ FaithfulSMul.{u_1, u_3} R[X] A[X]

Tactic:
(faithfulSMul_iff_algebraMap_injective ..).mpr
    (map_injective _ <| FaithfulSMul.algebraMap_injective ..)

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, Polynomial.map_injective, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
S_1 : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S_1
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S_1
inst_5 : Algebra S_1 A
inst_6 : IsScalarTower R S_1 A
S : Type u_4
inst_7 : CommSemiring S
inst_8 : Algebra R S
⊢ Algebra.IsPushout R R[X] S S[X]

Tactic:
.symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
S' : Type u
inst_7 : CommSemiring S'
inst_8 : Algebra R S'
φ : S →ₐ[R] S'
x : S ⊗[R] M
⊢ Eq (α := S' ⊗[R] N) ((rTensor N φ.toLinearMap : (a : S ⊗[R] N) → S' ⊗[R] N) (f.toFun' S x) : S' ⊗[R] N)
    (f.toFun' S' ((rTensor M φ.toLinearMap : (a : S ⊗[R] M) → S' ⊗[R] M) x) : S' ⊗[R] N)

Tactic:
simpa only using congr_fun (f.isCompat' φ) x

Premises used: congr_fun, PolynomialLaw.isCompat'
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ Eq (α := S ⊗[R] M → S ⊗[R] N) (toFun' 0 S) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u
inst_3 : CommSemiring S
inst_4 : Algebra R S
⊢ Eq (α := S ⊗[R] M → S ⊗[R] M) (toFun' id S) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ (f + g).toFun' S = HAdd.hAdd (α := S ⊗[R] M → S ⊗[R] N) (f.toFun' S) (g.toFun' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f g : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
m : S ⊗[R] M
⊢ (f + g).toFun' S m = f.toFun' S m + g.toFun' S m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ (r • f).toFun' S = HSMul.hSMul (β := S ⊗[R] M → S ⊗[R] N) r (f.toFun' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r : R
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
m : S ⊗[R] M
⊢ (r • f).toFun' S m = r • f.toFun' S m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
a b : R
f : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
    ((a + b) • f).toFun' x x_3 = (a • f + b • f).toFun' x x_3
⊢ (a + b) • f = a • f + b • f

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
a b : R
f : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ ((a + b) • f).toFun' x x_3 = (a • f + b • f).toFun' x x_3

Tactic:
simp only [add_def, smul_def, _root_.add_smul]

Premises used: PolynomialLaw.smul_def, PolynomialLaw.add_def, add_smul
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
toFun' :
  ∀ (S : Type u) (x : CommSemiring S) (x_1 : Algebra R S) (x_2 : S ⊗[R] M),
    (HSMul.hSMul (α := R) 0 f).toFun' S x_2 = PolynomialLaw.toFun' 0 S x_2
⊢ HSMul.hSMul (α := R) 0 f = 0

Tactic:
ext S
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
x_2 : S ⊗[R] M
⊢ (HSMul.hSMul (α := R) 0 f).toFun' S x_2 = toFun' 0 S x_2

Tactic:
simp only [smul_def, _root_.zero_smul, zero_def, Pi.zero_apply]

Premises used: PolynomialLaw.smul_def, Pi.zero_apply, PolynomialLaw.zero_def, zero_smul
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
toFun' :
  ∀ (S : Type u) (x : CommSemiring S) (x_1 : Algebra R S) (x_2 : S ⊗[R] M),
    (HSMul.hSMul (α := R) 1 f).toFun' S x_2 = f.toFun' S x_2
⊢ HSMul.hSMul (α := R) 1 f = f

Tactic:
ext S
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
x_2 : S ⊗[R] M
⊢ (HSMul.hSMul (α := R) 1 f).toFun' S x_2 = f.toFun' S x_2

Tactic:
simp only [smul_def, Pi.smul_apply, _root_.one_smul]

Premises used: PolynomialLaw.smul_def, one_smul, Pi.smul_apply
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a_1 b_1 : R
f_1 g : M →ₚₗ[R] N
a b : R
f : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
    ((a * b) • f).toFun' x x_3 = (a • b • f).toFun' x x_3
⊢ (a * b) • f = a • b • f

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a_1 b_1 : R
f_1 g : M →ₚₗ[R] N
a b : R
f : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ ((a * b) • f).toFun' x x_3 = (a • b • f).toFun' x x_3

Tactic:
simp only [smul_def, mul_smul]

Premises used: PolynomialLaw.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g_1 f g h : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
    (f + g + h).toFun' x x_3 = (f + (g + h)).toFun' x x_3
⊢ f + g + h = f + (g + h)

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g_1 f g h : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ (f + g + h).toFun' x x_3 = (f + (g + h)).toFun' x x_3

Tactic:
simp only [add_def, add_assoc]

Premises used: add_assoc, PolynomialLaw.add_def
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (0 + f).toFun' x x_3 = f.toFun' x x_3
⊢ 0 + f = f

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ (0 + f).toFun' x x_3 = f.toFun' x x_3

Tactic:
simp only [add_def, zero_add, zero_def]

Premises used: PolynomialLaw.zero_def, zero_add, PolynomialLaw.add_def
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (f + 0).toFun' x x_3 = f.toFun' x x_3
⊢ f + 0 = f

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ (f + 0).toFun' x x_3 = f.toFun' x x_3

Tactic:
simp only [add_def, add_zero, zero_def]

Premises used: PolynomialLaw.zero_def, PolynomialLaw.add_def, add_zero
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) (↑0 : R) f = 0

Tactic:
simp only [Nat.cast_zero, zero_smul f]

Premises used: PolynomialLaw.zero_smul, Nat.cast_zero
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) (↑(n + 1) : R) f = HSMul.hSMul (α := R) (↑n : R) f + f

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_smul, one_smul]

Premises used: PolynomialLaw.add_smul, PolynomialLaw.one_smul, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g_1 f g : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
    (f + g).toFun' x x_3 = (g + f).toFun' x x_3
⊢ f + g = g + f

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g_1 f g : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ (f + g).toFun' x x_3 = (g + f).toFun' x x_3

Tactic:
simp only [add_def, add_comm]

Premises used: add_comm, PolynomialLaw.add_def
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a_1 b : R
f_1 g_1 : M →ₚₗ[R] N
a : R
f g : M →ₚₗ[R] N
toFun' :
  ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
    (a • (f + g)).toFun' x x_3 = (a • f + a • g).toFun' x x_3
⊢ a • (f + g) = a • f + a • g

Tactic:
ext
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a_1 b : R
f_1 g_1 : M →ₚₗ[R] N
a : R
f g : M →ₚₗ[R] N
x : Type u
x_1 : CommSemiring x
x_2 : Algebra R x
x_3 : x ⊗[R] M
⊢ (a • (f + g)).toFun' x x_3 = (a • f + a • g).toFun' x x_3

Tactic:
simp only [smul_def, add_def, smul_add]

Premises used: PolynomialLaw.smul_def, PolynomialLaw.add_def, smul_add
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
⊢ (-f).toFun' S = HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) (f.toFun' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) (↑0 : R) f = 0

Tactic:
simp only [Int.cast_zero, zero_smul]

Premises used: Int.cast_zero, PolynomialLaw.zero_smul
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f = HSMul.hSMul (α := R) (↑(↑n : ℤ) : R) f + f

Tactic:
simp only [Nat.cast_succ, Int.cast_add, Int.cast_natCast,
    Int.cast_one, add_smul, _root_.one_smul]

Premises used: Nat.cast_succ, Int.cast_natCast, PolynomialLaw.add_smul, Int.cast_add, one_smul, Int.cast_one
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
toFun' :
  ∀ (S : Type u) (x : CommSemiring S) (x_1 : Algebra R S) (m : S ⊗[R] M),
    (HSMul.hSMul (α := R) (↑(Int.negSucc n) : R) f).toFun' S m =
      (-HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f).toFun' S m
⊢ HSMul.hSMul (α := R) (↑(Int.negSucc n) : R) f = -HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f

Tactic:
ext S _ _ m
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
toFun' :
  HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) =
    HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m)
⊢ (HSMul.hSMul (α := R) (↑(Int.negSucc n) : R) f).toFun' S m =
    HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) ((HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f).toFun' S) m

Tactic:
simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, _root_.add_smul,
      add_def_apply, smul_def_apply, Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast,
      Int.cast_one, _root_.one_smul, add_def, smul_def, Pi.smul_apply, Pi.add_apply, smul_add,
      smul_smul, neg_mul, one_mul]

Premises used: neg_add_rev, Int.cast_natCast, Nat.succ_eq_add_one, PolynomialLaw.smul_def, smul_smul, Int.cast_add, Int.cast_negSucc, one_smul, Pi.add_apply, PolynomialLaw.add_def_apply, Nat.cast_add, PolynomialLaw.add_def, add_smul, PolynomialLaw.smul_def_apply, neg_mul, Nat.cast_one, smul_add, one_mul, Int.cast_one, Pi.smul_apply
-- Module: Mathlib.RingTheory.PolynomialLaw.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
toFun' toFun'₁ :
  HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m) =
    HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m)
⊢ HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) =
    HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m)

Tactic:
rw [add_comm]

Premises used: add_comm