Theorem: MonoidAlgebra.rTensorAlgHom_apply_tmul_apply (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 α
n : N
a : α
⊢ (rTensorAlgHom (x ⊗ₜ[R] n)) a = x a ⊗ₜ[R] n
Tactic:
simp only [rTensorAlgHom]
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 α
n : N
a : α
⊢ ((Algebra.TensorProduct.lift (algHom Algebra.TensorProduct.includeLeft)
          (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) ⋯)
        (x ⊗ₜ[R] n))
      a =
    x a ⊗ₜ[R] n

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 α
n : N
a : α
⊢ ((Algebra.TensorProduct.lift (algHom Algebra.TensorProduct.includeLeft)
          (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) ⋯)
        (x ⊗ₜ[R] n))
      a =
    x a ⊗ₜ[R] n
Tactic:
simp only [Algebra.TensorProduct.lift_tmul]
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 α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x * (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) n) a =
    x a ⊗ₜ[R] n

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 α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x * (singleOneAlgHom.comp Algebra.TensorProduct.includeRight) n) a =
    x a ⊗ₜ[R] n
Tactic:
rw [AlgHom.comp_apply, singleOneAlgHom_apply, mul_single_one_apply]
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 α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * Algebra.TensorProduct.includeRight n = x a ⊗ₜ[R] n

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 α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * Algebra.TensorProduct.includeRight n = x a ⊗ₜ[R] n
Tactic:
simp only [Algebra.TensorProduct.includeRight_apply]
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 α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n

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 α
n : N
a : α
⊢ ((algHom Algebra.TensorProduct.includeLeft) x) a * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n
Tactic:
simp only [algHom_apply_apply, Algebra.TensorProduct.includeLeft_apply]
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 α
n : N
a : α
⊢ x a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n

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 α
n : N
a : α
⊢ x a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] n = x a ⊗ₜ[R] n
Tactic:
simp only [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul]
State after:
no goals