awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
refine_2 :
  ∀ (x : M) (x_1 : B),
    Eq (α := A ⊗[R] B[M])
      ((AlgHom.toLinearMap
                (AlgHom.comp (B := A ⊗[R] B[M])
                  (AlgHom.restrictScalars R
                    (AlgHom.comp tensorEquiv.invFun
                        (Algebra.TensorProduct.lift
                          (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
                          (mapAlgHom M includeRight) ⋯) :
                      A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
                  includeRight) ∘ₗ
              lsingle x :
            (a : B) → A ⊗[R] B[M])
          x_1 :
        A ⊗[R] B[M])
      (((AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight) ∘ₗ
                lsingle x :
              B →ₗ[R] A ⊗[R] B[M]) :
            (a : B) → A ⊗[R] B[M])
          x_1 :
        A ⊗[R] B[M])
⊢ Eq (α := B[M] →ₗ[R] A ⊗[R] B[M])
    (AlgHom.toLinearMap
      (AlgHom.comp (B := A ⊗[R] B[M])
        (AlgHom.restrictScalars R
          (AlgHom.comp tensorEquiv.invFun
              (Algebra.TensorProduct.lift
                (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
                (mapAlgHom M includeRight) ⋯) :
            A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
        includeRight))
    (AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight))

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
x : M
x_1 : B
⊢ Eq (α := A ⊗[R] B[M])
    ((AlgHom.toLinearMap
              (AlgHom.comp (B := A ⊗[R] B[M])
                (AlgHom.restrictScalars R
                  (AlgHom.comp tensorEquiv.invFun
                      (Algebra.TensorProduct.lift
                        (AlgHom.comp (B := A ⊗[R] B) (IsScalarTower.toAlgHom A (A ⊗[R] B) (A ⊗[R] B)[M]) includeLeft)
                        (mapAlgHom M includeRight) ⋯) :
                    A ⊗[R] B[M] →ₐ[A] A ⊗[R] B[M]))
                includeRight) ∘ₗ
            lsingle x :
          (a : B) → A ⊗[R] B[M])
        x_1 :
      A ⊗[R] B[M])
    (((AlgHom.toLinearMap (AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] B[M]))) includeRight) ∘ₗ
              lsingle x :
            B →ₗ[R] A ⊗[R] B[M]) :
          (a : B) → A ⊗[R] B[M])
        x_1 :
      A ⊗[R] B[M])

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CommMonoid M
a : A
p : B[M]
⊢ (tensorEquiv R A B : (a : A ⊗[R] B[M]) → (A ⊗[R] B)[M]) (a ⊗ₜ[R] p) =
    HSMul.hSMul (β := (A ⊗[R] B)[M]) a ((mapAlgHom M includeRight : (a : B[M]) → (A ⊗[R] B)[M]) p : (A ⊗[R] B)[M])

Tactic:
simp [tensorEquiv, Algebra.smul_def]

Premises used: MonoidAlgebra.tensorEquiv, Algebra.smul_def
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : CommMonoid M
m : M
a : A
b : B
⊢ Eq (α := A ⊗[R] B[M])
    ((AlgEquiv.symm (tensorEquiv R A B) : (a : (A ⊗[R] B)[M]) → A ⊗[R] B[M]) (single m (a ⊗ₜ[R] b)) : A ⊗[R] B[M])
    (a ⊗ₜ[R] single m b : A ⊗[R] B[M])

Tactic:
tensorEquiv.invFun_tmul ..

Premises used: Multiset.sum, Multiset.foldr, MonoidAlgebra.tensorEquiv.invFun_tmul, Finsupp.sum, Finset.sum
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommMonoid M
a : A
p : R[M]
hfg :
  ∀ (m : M),
    Eq.{u_4 + 1} (α := A)
      ((((scalarTensorEquiv R A : (a : A ⊗[R] R[M]) → A[M]) (a ⊗ₜ[R] p) : A[M]) : (a : M) → A) m : A)
      ((HSMul.hSMul (β := A[M]) a ((mapAlgHom M (ofId R A) : (a : R[M]) → A[M]) p : A[M]) : (a : M) → A) m : A)
⊢ (scalarTensorEquiv R A : (a : A ⊗[R] R[M]) → A[M]) (a ⊗ₜ[R] p) =
    HSMul.hSMul (β := A[M]) a ((mapAlgHom M (ofId R A) : (a : R[M]) → A[M]) p : A[M])

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommMonoid M
a : A
p : R[M]
m : M
hfg :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : M) → R) m : R) a =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) ((p : (a : M) → R) m : R) : A)
⊢ Eq.{u_4 + 1} (α := A) ((((scalarTensorEquiv R A : (a : A ⊗[R] R[M]) → A[M]) (a ⊗ₜ[R] p) : A[M]) : (a : M) → A) m : A)
    ((HSMul.hSMul (β := A[M]) a ((mapAlgHom M (ofId R A) : (a : R[M]) → A[M]) p : A[M]) : (a : M) → A) m : A)

Tactic:
simp [scalarTensorEquiv]

Premises used: MonoidAlgebra.scalarTensorEquiv
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommMonoid M
a : A
p : R[M]
m : M
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : M) → R) m : R) a =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) ((p : (a : M) → R) m : R) : A)

Tactic:
simp [Algebra.smul_def, Algebra.commutes]

Premises used: Algebra.smul_def, Algebra.commutes
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
A : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : CommMonoid M
m : M
a : A
⊢ Eq (α := A ⊗[R] R[M]) ((AlgEquiv.symm (scalarTensorEquiv R A) : (a : A[M]) → A ⊗[R] R[M]) (single m a) : A ⊗[R] R[M])
    (a ⊗ₜ[R] single m 1 : A ⊗[R] R[M])

Tactic:
simp [scalarTensorEquiv]

Premises used: MonoidAlgebra.scalarTensorEquiv
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
x : A[M]
zero :
  Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] 0) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) 0 : B[M])
add :
  ∀ (x y : A[M]),
    Eq (α := B[M])
        (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
              (a : S ⊗[R] A[M]) → B[M])
            (1 ⊗ₜ[R] x) :
          B[M])
        ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M]) →
      Eq (α := B[M])
          (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) :
                  S ⊗[R] A[M] ≃ₗ[S] B[M]) :
                (a : S ⊗[R] A[M]) → B[M])
              (1 ⊗ₜ[R] y) :
            B[M])
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) y : B[M]) →
        Eq (α := B[M])
          (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) :
                  S ⊗[R] A[M] ≃ₗ[S] B[M]) :
                (a : S ⊗[R] A[M]) → B[M])
              (1 ⊗ₜ[R] (x + y)) :
            B[M])
          ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (x + y) : B[M])
single :
  ∀ (m : M) (r : A),
    Eq (α := B[M])
      (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
            (a : S ⊗[R] A[M]) → B[M])
          (1 ⊗ₜ[R] MonoidAlgebra.single m r) :
        B[M])
      ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (MonoidAlgebra.single m r) : B[M])
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] x) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M])

Tactic:
induction x using induction_linear
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] 0) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) 0 : B[M])

Tactic:
simp_all [IsPushout.equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
x y : A[M]
h :
  Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] x) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) x : B[M])
h_1 :
  Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] y) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) y : B[M])
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] (x + y)) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (x + y) : B[M])

Tactic:
simp_all [IsPushout.equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R S A B
m : M
r : A
⊢ Eq (α := B[M])
    (((↑(AlgEquiv.trans (tensorEquiv R S A) (mapAlgEquiv S M (IsPushout.equiv R S A B))) : S ⊗[R] A[M] ≃ₗ[S] B[M]) :
          (a : S ⊗[R] A[M]) → B[M])
        (1 ⊗ₜ[R] single m r) :
      B[M])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R A[M] B[M]) : (a : A[M]) → B[M]) (single m r) : B[M])

Tactic:
simp_all [IsPushout.equiv_tmul]

Premises used: Algebra.IsPushout.equiv_tmul
-- Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring A
inst_3 : CommSemiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : CommMonoid M
inst_8 : Algebra S B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
inst_11 : IsScalarTower R S B
inst_12 : IsPushout R A S B
⊢ IsPushout R A[M] S B[M]

Tactic:
have : IsPushout R S A B := .symm ‹_›; .symm inferInstance

Premises used: inferInstance, Algebra.IsPushout.symm
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
p : MvPolynomial σ S
n : N
⊢ Eq (α := (σ →₀ ℕ) →₀ S ⊗[R] N)
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) (p ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N)
    (Finsupp.sum p fun (i : σ →₀ ℕ) (m : S) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N)

Tactic:
TensorProduct.finsuppLeft_apply_tmul p n

Premises used: TensorProduct.finsuppLeft_apply_tmul, AddMonoidAlgebra
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) (p ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    (coeff d p ⊗ₜ[R] n : S ⊗[R] N)

Tactic:
TensorProduct.finsuppLeft_apply_tmul_apply p n d

Premises used: MvPolynomial.coeff, AddMonoidAlgebra, TensorProduct.finsuppLeft_apply_tmul_apply
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
e : σ →₀ ℕ
s : S
n : N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N)
              ((monomial e : (a : S) → MvPolynomial σ S) s ⊗ₜ[R] n) :
            (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    (if e = d then s ⊗ₜ[R] n else 0 : S ⊗[R] N)

Tactic:
simp only [rTensor_apply_tmul_apply, coeff_monomial, ite_tmul]

Premises used: MvPolynomial.rTensor_apply_tmul_apply, TensorProduct.ite_tmul, MvPolynomial.coeff_monomial
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : Eq (α := S ⊗[R] N) (coeff d (X s) ⊗ₜ[R] n) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
rw₁ :
  Eq (α := S ⊗[R] N) ((if Finsupp.single s 1 = d then 1 else 0) ⊗ₜ[R] n)
    (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
rw₂ rw₃ :
  Eq (α := S ⊗[R] N) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0) (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0)
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) (X s ⊗ₜ[R] n) : (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    (if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0 : S ⊗[R] N)

Tactic:
rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul]

Premises used: MvPolynomial.rTensor_apply_tmul_apply, TensorProduct.ite_tmul, MvPolynomial.coeff_X'
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
t : MvPolynomial σ S ⊗[R] N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    ((((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) t : (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        d :
      S ⊗[R] N)
    ((LinearMap.rTensor N
            ((↑R :
                {S : Type u_3} →
                  {M : Type (max u_1 u_3)} →
                    {M₂ : Type u_3} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (lcoeff S d)) :
          (a : MvPolynomial σ S ⊗[R] N) → S ⊗[R] N)
        t :
      S ⊗[R] N)

Tactic:
TensorProduct.finsuppLeft_apply t d

Premises used: TensorProduct.finsuppLeft_apply, MvPolynomial.coeff, AddMonoidAlgebra
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : DecidableEq σ
inst_4 : AddCommMonoid N
inst_5 : Module R N
d : σ →₀ ℕ
s : S
n : N
⊢ Eq (α := MvPolynomial σ S ⊗[R] N)
    ((LinearEquiv.symm rTensor : (a : (σ →₀ ℕ) →₀ S ⊗[R] N) → MvPolynomial σ S ⊗[R] N) (Finsupp.single d (s ⊗ₜ[R] n)) :
      MvPolynomial σ S ⊗[R] N)
    ((monomial d : (a : S) → MvPolynomial σ S) s ⊗ₜ[R] n : MvPolynomial σ S ⊗[R] N)

Tactic:
TensorProduct.finsuppLeft_symm_apply_single (R := R) d s n

Premises used: TensorProduct.finsuppLeft_symm_apply_single, AddMonoidAlgebra, Finsupp.single
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : MvPolynomial σ R
n : N
⊢ Eq (α := Finsupp.{u_1, v} (σ →₀ ℕ) N)
    ((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (p ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N)
    (Finsupp.sum p fun (i : σ →₀ ℕ) (m : R) ↦ Finsupp.single i (m • n) : Finsupp.{u_1, v} (σ →₀ ℕ) N)

Tactic:
TensorProduct.finsuppScalarLeft_apply_tmul p n

Premises used: TensorProduct.finsuppScalarLeft_apply_tmul, AddMonoidAlgebra
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
p : MvPolynomial σ R
n : N
d : σ →₀ ℕ
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (p ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    coeff d p • n

Tactic:
TensorProduct.finsuppScalarLeft_apply_tmul_apply p n d

Premises used: MvPolynomial.coeff, TensorProduct.finsuppScalarLeft_apply_tmul_apply, AddMonoidAlgebra
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
e : σ →₀ ℕ
r : R
n : N
d : σ →₀ ℕ
rw :
  HSMul.hSMul.{u, v, v} (α := R) (coeff d ((monomial e : (a : R) → MvPolynomial σ R) r)) n = if e = d then r • n else 0
rw₁ : (if e = d then r else 0) • n = if e = d then r • n else 0
rw₂ : (if e = d then r • n else HSMul.hSMul.{u, v, v} (α := R) 0 n) = if e = d then r • n else 0
rw₃ rw₄ : (if e = d then r • n else 0) = if e = d then r • n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N)
            ((monomial e : (a : R) → MvPolynomial σ R) r ⊗ₜ[R] n) :
          Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if e = d then r • n else 0

Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]

Premises used: zero_smul, ite_smul, MvPolynomial.coeff_monomial, MvPolynomial.scalarRTensor_apply_tmul_apply
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d (X s)) n = if Finsupp.single s 1 = d then n else 0
rw₁ :
  HSMul.hSMul.{u, v, v} (α := R) (if Finsupp.single s 1 = d then 1 else 0) n = if Finsupp.single s 1 = d then n else 0
rw₂ :
  (if Finsupp.single s 1 = d then HSMul.hSMul.{u, v, v} (α := R) 1 n else HSMul.hSMul.{u, v, v} (α := R) 0 n) =
    if Finsupp.single s 1 = d then n else 0
rw₃ :
  (if Finsupp.single s 1 = d then n else HSMul.hSMul.{u, v, v} (α := R) 0 n) = if Finsupp.single s 1 = d then n else 0
rw₄ rw₅ : (if Finsupp.single s 1 = d then n else 0) = if Finsupp.single s 1 = d then n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (X s ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if Finsupp.single s 1 = d then n else 0

Tactic:
rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]

Premises used: one_smul, zero_smul, MvPolynomial.coeff_X', ite_smul, MvPolynomial.scalarRTensor_apply_tmul_apply
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
d : σ →₀ ℕ
n : N
⊢ Eq (α := MvPolynomial σ R ⊗[R] N)
    ((LinearEquiv.symm scalarRTensor : (a : (σ →₀ ℕ) →₀ N) → MvPolynomial σ R ⊗[R] N) (Finsupp.single d n) :
      MvPolynomial σ R ⊗[R] N)
    ((monomial d : (a : R) → MvPolynomial σ R) 1 ⊗ₜ[R] n : MvPolynomial σ R ⊗[R] N)

Tactic:
TensorProduct.finsuppScalarLeft_symm_apply_single d n

Premises used: AddMonoidAlgebra, TensorProduct.finsuppScalarLeft_symm_apply_single, Finsupp.single
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
p : MvPolynomial σ S
n : N
⊢ Commute (S := MvPolynomial σ (S ⊗[R] N))
    ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p :
      MvPolynomial σ (S ⊗[R] N))
    ((AlgHom.comp (B := S ⊗[R] N) (IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N)))
            Algebra.TensorProduct.includeRight :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n :
      MvPolynomial σ (S ⊗[R] N))

Tactic:
simp [commute_iff_eq, algebraMap_eq, mul_comm]

Premises used: commute_iff_eq, MvPolynomial.algebraMap_eq, mul_comm
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
rw :
  coeff d
      (HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
        ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p :
          MvPolynomial σ (S ⊗[R] N))
        ((AlgHom.comp (B := S ⊗[R] N) (IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N)))
                Algebra.TensorProduct.includeRight :
              (a : N) → MvPolynomial σ (S ⊗[R] N))
            n :
          MvPolynomial σ (S ⊗[R] N))) =
    coeff d p ⊗ₜ[R] n
⊢ Eq (α := S ⊗[R] N) (coeff d ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (p ⊗ₜ[R] n)))
    (coeff d p ⊗ₜ[R] n)

Tactic:
rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]

Premises used: MvPolynomial.rTensorAlgHom, Algebra.TensorProduct.lift_tmul