Theorem: MonoidAlgebra.rTensorAlgHom_apply_eq (DividedPowers/ForMathlib/RingTheory/TensorProduct/MonoidAlgebra.lean)

State before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α ⊗[R] N
⊢ rTensorAlgHom x = (finsuppLeft' R M N α S) x
Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
State after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α ⊗[R] N
⊢ ↑(finsuppLeft' R M N α S) x = (finsuppLeft' R M N α S) x

State before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
x : MonoidAlgebra M α ⊗[R] N
⊢ ↑(finsuppLeft' R M N α S) x = (finsuppLeft' R M N α S) x
Tactic:
rfl
State after:
no goals