Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hl
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₂
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
              AlgebraTensorModule.lift
                (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                  (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃))))
          x✝¹ ∘ₗ
        LinearMap.inl R M₂ M₃)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹ ∘ₗ LinearMap.inl R M₂ M₃) x✝

pp: case hr
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₃
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
              AlgebraTensorModule.lift
                (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                  (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃))))
          x✝¹ ∘ₗ
        LinearMap.inr R M₂ M₃)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹ ∘ₗ LinearMap.inr R M₂ M₃) x✝

Tactic:
<;>

Goal state after:
case hl
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₂
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
              AlgebraTensorModule.lift
                (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                  (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃))))
          x✝¹ ∘ₗ
        LinearMap.inl R M₂ M₃)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹ ∘ₗ LinearMap.inl R M₂ M₃) x✝

case hr
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Algebra R S
inst✝⁴ : Module R M₁
inst✝³ : Module S M₁
inst✝² : IsScalarTower R S M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
x✝¹ : M₁
x✝ : M₃
⊢ ((AlgebraTensorModule.curry
            (((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃)) ∘ₗ
              AlgebraTensorModule.lift
                (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                  (AlgebraTensorModule.mk R S M₁ M₂).prod (AlgebraTensorModule.mk R S M₁ M₃))))
          x✝¹ ∘ₗ
        LinearMap.inr R M₂ M₃)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id) x✝¹ ∘ₗ LinearMap.inr R M₂ M₃) x✝