Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap (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
⊢ rTensorAlgHom.toLinearMap = ↑(finsuppLeft' R M N α S)
Tactic:
ext x n
State after:
case a.h.h
α : 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 α
n : N
⊢ ((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap) x) n =
    ((AlgebraTensorModule.curry ↑(finsuppLeft' R M N α S)) x) n

State before:
case a.h.h
α : 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 α
n : N
⊢ ((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap) x) n =
    ((AlgebraTensorModule.curry ↑(finsuppLeft' R M N α S)) x) n
Tactic:
dsimp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
  LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
State after:
case a.h.h
α : 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 α
n : N
⊢ rTensorAlgHom (x ⊗ₜ[R] n) = ↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)

State before:
case a.h.h
α : 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 α
n : N
⊢ rTensorAlgHom (x ⊗ₜ[R] n) = ↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)
Tactic:
apply Finsupp.ext
State after:
case a.h.h.h
α : 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 α
n : N
⊢ ∀ (a : α), (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a

State before:
case a.h.h.h
α : 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 α
n : N
⊢ ∀ (a : α), (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Tactic:
intro a
State after:
case a.h.h.h
α : 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 α
n : N
a : α
⊢ (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a

State before:
case a.h.h.h
α : 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 α
n : N
a : α
⊢ (rTensorAlgHom (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Tactic:
rw [rTensorAlgHom_apply_tmul_apply, ← finsuppLeft_apply_tmul_apply]
State after:
case a.h.h.h
α : 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 α
n : N
a : α
⊢ ((finsuppLeft R M N α) (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a

State before:
case a.h.h.h
α : 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 α
n : N
a : α
⊢ ((finsuppLeft R M N α) (x ⊗ₜ[R] n)) a = (↑(finsuppLeft' R M N α S) (x ⊗ₜ[R] n)) a
Tactic:
rfl
State after:
no goals