-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma rTensorAlgHom_toLinearMap :
    (rTensorAlgHom :
      MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)).toLinearMap =
      rTensor.toLinearMap

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
⊢ rTensorAlgHom.toLinearMap = ↑rTensor

Tactic:
ext d n e

Result:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) =
    coeff e (((AlgebraTensorModule.curry ↑rTensor ∘ₗ monomial d) 1) n)

Proof state:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) =
    coeff e (((AlgebraTensorModule.curry ↑rTensor ∘ₗ monomial d) 1) n)

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

Result:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑rTensor ((monomial d) 1 ⊗ₜ[R] n))

Proof state:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (rTensorAlgHom ((monomial d) 1 ⊗ₜ[R] n)) = coeff e (↑rTensor ((monomial d) 1 ⊗ₜ[R] n))

Tactic:
rw [coeff_rTensorAlgHom_tmul]

Result:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑rTensor ((monomial d) 1 ⊗ₜ[R] n))

Proof state:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ ((monomial d) 1) e ⊗ₜ[R] n = (↑rTensor ((monomial d) 1 ⊗ₜ[R] n)) e

Tactic:
erw [finsuppLeft_apply_tmul_apply]

Result:
no goals

Proof state:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e ((monomial d) 1) ⊗ₜ[R] n = coeff e (↑rTensor ((monomial d) 1 ⊗ₜ[R] n))

Tactic:
simp only [coeff]

Result:
case a.h.h.h.a
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : CommSemiring N
inst✝¹ : Algebra R N
inst✝ : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ ((monomial d) 1) e ⊗ₜ[R] n = (↑rTensor ((monomial d) 1 ⊗ₜ[R] n)) e