awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  HMul.hMul (α := S ⊗[R] N) (1 ⊗ₜ[R] n)
      (coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p)) =
    coeff d p ⊗ₜ[R] n
⊢ 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))
        ((algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N)) : (a : S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] n) :
          MvPolynomial σ (S ⊗[R] N))) =
    coeff d p ⊗ₜ[R] n

Tactic:
rw [algebraMap_eq, mul_comm, coeff_C_mul]

Premises used: MvPolynomial.coeff_C_mul, 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 : σ →₀ ℕ
⊢ HMul.hMul (α := S ⊗[R] N) (1 ⊗ₜ[R] n)
      (coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p)) =
    coeff d p ⊗ₜ[R] n

Tactic:
simp [coeff_map]

Premises used: MvPolynomial.coeff_map
-- 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
inst_5 : DecidableEq σ
e : σ →₀ ℕ
s : S
n : N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (coeff d
      ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((monomial e : (a : S) → MvPolynomial σ S) s ⊗ₜ[R] n)))
    (if e = d then s ⊗ₜ[R] n else 0)

Tactic:
simp [ite_tmul]

Premises used: TensorProduct.ite_tmul
-- 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
inst_5 : DecidableEq σ
a :
  ∀ (d : σ →₀ ℕ) (n : N) (e : σ →₀ ℕ),
    Eq (α := S ⊗[R] N)
      (coeff e
        ((((AlgebraTensorModule.curry (AlgHom.toLinearMap rTensorAlgHom) ∘ₗ AddMonoidAlgebra.lsingle d :
                  S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
                (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
              1 :
            (a : N) → MvPolynomial σ (S ⊗[R] N))
          n))
      (coeff e
        ((((AlgebraTensorModule.curry (↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) ∘ₗ
                    AddMonoidAlgebra.lsingle d :
                  S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
                (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
              1 :
            (a : N) → MvPolynomial σ (S ⊗[R] N))
          n))
⊢ Eq (α := MvPolynomial σ S ⊗[R] N →ₗ[S] MvPolynomial σ (S ⊗[R] N)) (AlgHom.toLinearMap rTensorAlgHom)
    (↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N)

Tactic:
ext d n e
-- 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
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
a :
  Eq (α := S ⊗[R] N)
    (coeff e
      ((rTensorAlgHom : (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
    (coeff e
      (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
⊢ Eq (α := S ⊗[R] N)
    (coeff e
      ((((AlgebraTensorModule.curry (AlgHom.toLinearMap rTensorAlgHom) ∘ₗ AddMonoidAlgebra.lsingle d :
                S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
              (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
            1 :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n))
    (coeff e
      ((((AlgebraTensorModule.curry (↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) ∘ₗ
                  AddMonoidAlgebra.lsingle d :
                S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
              (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
            1 :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n))

Tactic:
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
    LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]

Premises used: LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply, TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.coe_comp, TensorProduct.curry_apply, Function.comp_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 : CommSemiring N
inst_4 : Algebra R N
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
a :
  Eq (α := S ⊗[R] N) (coeff e ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1) ⊗ₜ[R] n)
    (coeff e
      (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
⊢ Eq (α := S ⊗[R] N)
    (coeff e
      ((rTensorAlgHom : (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
    (coeff e
      (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))

Tactic:
rw [coeff_rTensorAlgHom_tmul]

Premises used: MvPolynomial.coeff_rTensorAlgHom_tmul
-- 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
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
a :
  Eq (α := S ⊗[R] N)
    (((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 : (a : σ →₀ ℕ) → S) e ⊗ₜ[R] n : S ⊗[R] N)
    (((((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
                (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
              ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n) :
            MvPolynomial σ (S ⊗[R] N)) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        e :
      S ⊗[R] N)
⊢ Eq (α := S ⊗[R] N) (coeff e ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1) ⊗ₜ[R] n)
    (coeff e
      (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))

Tactic:
simp only [coeff]

Premises used: MvPolynomial.coeff
-- 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
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 : (a : σ →₀ ℕ) → S) e ⊗ₜ[R] n : S ⊗[R] N)
    (((((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
                (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
              ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n) :
            MvPolynomial σ (S ⊗[R] N)) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        e :
      S ⊗[R] N)

Tactic:
(finsuppLeft_apply_tmul_apply _ _ _).symm

Premises used: AddMonoidAlgebra, Eq.symm, 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 : CommSemiring N
inst_4 : Algebra R N
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 : (a : σ →₀ ℕ) → S) e ⊗ₜ[R] n : S ⊗[R] N)
    (((((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
                (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
              ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n) :
            MvPolynomial σ (S ⊗[R] N)) :
          (a : σ →₀ ℕ) → S ⊗[R] N)
        e :
      S ⊗[R] N)

Tactic:
exact (finsuppLeft_apply_tmul_apply _ _ _).symm

Premises used: Eq.symm, 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 : CommSemiring N
inst_4 : Algebra R N
inst_5 : DecidableEq σ
p : MvPolynomial σ S ⊗[R] N
rw :
  Eq (α := MvPolynomial σ (S ⊗[R] N))
    (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        p :
      MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) p : (σ →₀ ℕ) →₀ S ⊗[R] N)
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) p : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) p : (σ →₀ ℕ) →₀ S ⊗[R] N)

Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]

Premises used: AlgHom.toLinearMap_apply, MvPolynomial.rTensorAlgHom_toLinearMap
-- 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
inst_5 : DecidableEq σ
p : MvPolynomial σ S ⊗[R] N
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        p :
      MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) p : (σ →₀ ℕ) →₀ S ⊗[R] N)

Tactic:
rfl
-- 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
inst_5 : DecidableEq σ
map_one :
  Eq (α := MvPolynomial σ (S ⊗[R] N)) ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) 1) 1
map_mul :
  ∀ (x y : MvPolynomial σ S ⊗[R] N),
    (rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
      HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
        ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
        ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
⊢ MvPolynomial σ S ⊗[R] N ≃ₐ[S] MvPolynomial σ (S ⊗[R] N)

Tactic:
apply AlgEquiv.ofLinearEquiv rTensor

Premises used: AlgEquiv.ofLinearEquiv
-- 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
inst_5 : DecidableEq σ
map_one :
  Eq (α := MvPolynomial σ (S ⊗[R] N)) (1 : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] 1) : MvPolynomial σ (S ⊗[R] N))
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] 1) : MvPolynomial σ (S ⊗[R] N))
    (1 : MvPolynomial σ (S ⊗[R] N))

Tactic:
apply symm

Premises used: symm
-- 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
inst_5 : DecidableEq σ
map_one :
  Eq (α := MvPolynomial σ S ⊗[R] N)
    ((LinearEquiv.symm rTensor : (a : MvPolynomial σ (S ⊗[R] N)) → MvPolynomial σ S ⊗[R] N) 1) (1 ⊗ₜ[R] 1)
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N)) (1 : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] 1) : MvPolynomial σ (S ⊗[R] N))

Tactic:
rw [← LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- 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
inst_5 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ S ⊗[R] N)
    ((LinearEquiv.symm rTensor : (a : MvPolynomial σ (S ⊗[R] N)) → MvPolynomial σ S ⊗[R] N) 1) (1 ⊗ₜ[R] 1)

Tactic:
finsuppLeft_symm_apply_single (R := R) (0 : σ →₀ ℕ) (1 : S) (1 : N)

Premises used: TensorProduct.finsuppLeft_symm_apply_single, AddMonoidAlgebra, OfNat.ofNat, 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
inst_5 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ S ⊗[R] N)
    ((LinearEquiv.symm rTensor : (a : MvPolynomial σ (S ⊗[R] N)) → MvPolynomial σ S ⊗[R] N) 1) (1 ⊗ₜ[R] 1)

Tactic:
exact finsuppLeft_symm_apply_single (R := R) (0 : σ →₀ ℕ) (1 : S) (1 : N)

Premises used: TensorProduct.finsuppLeft_symm_apply_single, OfNat.ofNat
-- 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
inst_5 : DecidableEq σ
x y : MvPolynomial σ S ⊗[R] N
map_mul :
  (rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
⊢ (rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))

Tactic:
erw [← rTensorAlgHom_apply_eq (S := S)]

Premises used: MvPolynomial.rTensorAlgHom_apply_eq
-- 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
inst_5 : DecidableEq σ
x y : MvPolynomial σ S ⊗[R] N
map_mul :
  HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) x : (σ →₀ ℕ) →₀ S ⊗[R] N)
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) y : (σ →₀ ℕ) →₀ S ⊗[R] N) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
⊢ (rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))

Tactic:
simp only [map_mul, rTensorAlgHom_apply_eq]

Premises used: map_mul, MvPolynomial.rTensorAlgHom_apply_eq
-- 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
inst_5 : DecidableEq σ
x y : MvPolynomial σ S ⊗[R] N
⊢ HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) x : (σ →₀ ℕ) →₀ S ⊗[R] N)
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) y : (σ →₀ ℕ) →₀ S ⊗[R] N) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))

Tactic:
rfl
-- 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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
e_a : (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) = rTensorAlgHom
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    (((↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) :
          (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        x :
      MvPolynomial σ (S ⊗[R] N))
    ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))

Tactic:
congr 1
-- 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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
e_a :
  ∀ (i : σ) (d : σ →₀ ℕ),
    Eq (α := S ⊗[R] N)
      (coeff d
        ((AlgHom.comp (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N))
              Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
          (X i)))
      (coeff d
        ((AlgHom.comp rTensorAlgHom Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
          (X i)))
e_a₁ :
  ∀ (x : N) (d : σ →₀ ℕ),
    Eq (α := S ⊗[R] N)
      (coeff d
        ((AlgHom.comp
              (AlgHom.restrictScalars R (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)))
              Algebra.TensorProduct.includeRight :
            (a : N) → MvPolynomial σ (S ⊗[R] N))
          x))
      (coeff d
        ((AlgHom.comp (AlgHom.restrictScalars R rTensorAlgHom) Algebra.TensorProduct.includeRight :
            (a : N) → MvPolynomial σ (S ⊗[R] N))
          x))
⊢ (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) = rTensorAlgHom

Tactic:
ext _ d
-- 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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
i : σ
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (coeff d
      ((AlgHom.comp (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N))
            Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
        (X i)))
    (coeff d
      ((AlgHom.comp rTensorAlgHom Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
        (X i)))

Tactic:
simpa [rTensorAlgEquiv] using rTensor_apply_tmul_apply _ _ d

Premises used: MvPolynomial.rTensor_apply_tmul_apply, MvPolynomial.rTensorAlgEquiv
-- 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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
x_1 : N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (coeff d
      ((AlgHom.comp
            (AlgHom.restrictScalars R (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)))
            Algebra.TensorProduct.includeRight :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        x_1))
    (coeff d
      ((AlgHom.comp (AlgHom.restrictScalars R rTensorAlgHom) Algebra.TensorProduct.includeRight :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        x_1))

Tactic:
simpa [rTensorAlgEquiv] using rTensor_apply_tmul_apply _ _ d

Premises used: MvPolynomial.rTensor_apply_tmul_apply, MvPolynomial.rTensorAlgEquiv
-- 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
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
hf :
  ∀ (s : σ) (m : σ →₀ ℕ),
    Eq.{u_4 + 1} (α := A)
      (coeff m
        ((AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
              (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯ :
                A ⊗[R] MvPolynomial σ R →ₐ[A] MvPolynomial σ A)
              (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R) :
            (a : MvPolynomial σ A) → MvPolynomial σ A)
          (X s)))
      (coeff m ((AlgHom.id A (MvPolynomial σ A) : (a : MvPolynomial σ A) → MvPolynomial σ A) (X s)))
⊢ Eq (α := MvPolynomial σ A →ₐ[A] MvPolynomial σ A)
    (AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
      (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯ :
        A ⊗[R] MvPolynomial σ R →ₐ[A] MvPolynomial σ A)
      (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
    (AlgHom.id A (MvPolynomial σ A))

Tactic:
ext s
-- 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
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
s : σ
m : σ →₀ ℕ
⊢ Eq.{u_4 + 1} (α := A)
    (coeff m
      ((AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
            (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯ :
              A ⊗[R] MvPolynomial σ R →ₐ[A] MvPolynomial σ A)
            (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R) :
          (a : MvPolynomial σ A) → MvPolynomial σ A)
        (X s)))
    (coeff m ((AlgHom.id A (MvPolynomial σ A) : (a : MvPolynomial σ A) → MvPolynomial σ A) (X s)))

Tactic:
simp