Module: Mathlib.LinearAlgebra.TensorProduct.Prod

Goal state before:
pp: case hl.fst
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).1 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).1

pp: case hl.snd
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).2 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).2

pp: case hr.fst
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).1 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).1

pp: case hr.snd
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).2 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).2

Tactic:
<;>

Goal state after:
case hl.fst
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).1 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).1

case hl.snd
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).2 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).2

case hr.fst
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).1 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).1

case hr.snd
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.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₃)) ∘ₗ
                ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inl R M₂ M₃)).coprod
                  ((AlgebraTensorModule.lTensor S M₁) (LinearMap.inr R M₂ M₃))) ∘ₗ
              LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)))
          x✝¹)
        x✝).2 =
    (((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃))) x✝¹) x✝).2