Module: Mathlib.RingTheory.TensorProduct.MonoidAlgebra

Goal state before:
pp: case zero
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] 0) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap 0

pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
x✝ y✝ : A[M]
a✝¹ :
  ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] x✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap x✝
a✝ :
  ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] y✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap y✝
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap (x✝ + y✝)

pp: case single
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
m✝ : M
r✝ : A
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] single m✝ r✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap (single m✝ r✝)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] 0) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap 0

case add
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
x✝ y✝ : A[M]
a✝¹ :
  ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] x✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap x✝
a✝ :
  ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] y✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap y✝
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] (x✝ + y✝)) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap (x✝ + y✝)

case single
R : Type u_1
M : Type u_2
N : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : CommSemiring S
inst✝¹³ : CommSemiring A
inst✝¹² : CommSemiring B
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra S A
inst✝⁷ : IsScalarTower R S A
inst✝⁶ : CommMonoid M
inst✝⁵ : CommMonoid N
inst✝⁴ : Algebra S B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : IsPushout R S A B
m✝ : M
r✝ : A
⊢ ↑((rTensorEquivAlgEquiv R S S A).trans (mapAlgEquiv S M (IsPushout.equiv R S A B))) (1 ⊗ₜ[R] single m✝ r✝) =
    (IsScalarTower.toAlgHom R A[M] B[M]).toLinearMap (single m✝ r✝)