-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
hl :
  ∀ (x : M₁) (x_1 : M₂),
    Eq (α := M₁ ⊗[R] M₂)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.lift
                              (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                                LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
                            M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
                          (LinearMap.coprod
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inl R M₂ M₃))
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inr R M₂ M₃)) :
                            M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                        LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).1
      (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).1
hl₁ :
  ∀ (x : M₁) (x_1 : M₂),
    Eq (α := M₁ ⊗[R] M₃)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.lift
                              (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                                LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
                            M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
                          (LinearMap.coprod
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inl R M₂ M₃))
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inr R M₂ M₃)) :
                            M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                        LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).2
      (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).2
hr :
  ∀ (x : M₁) (x_1 : M₃),
    Eq (α := M₁ ⊗[R] M₂)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.lift
                              (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                                LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
                            M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
                          (LinearMap.coprod
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inl R M₂ M₃))
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inr R M₂ M₃)) :
                            M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                        LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).1
      (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).1
hr₁ :
  ∀ (x : M₁) (x_1 : M₃),
    Eq (α := M₁ ⊗[R] M₃)
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.lift
                              (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                                LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
                            M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
                          (LinearMap.coprod
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inl R M₂ M₃))
                              (((AlgebraTensorModule.lTensor S M₁ :
                                    (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                                  (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                                (LinearMap.inr R M₂ M₃)) :
                            M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                        LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).2
      (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                    M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                  (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
                x :
              M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
            (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
          x_1).2
⊢ Eq (α := M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
    ((AlgebraTensorModule.lift
          (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
            LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
        M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) ∘ₗ
      (LinearMap.coprod
          (((AlgebraTensorModule.lTensor S M₁ : (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
              (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
            (LinearMap.inl R M₂ M₃))
          (((AlgebraTensorModule.lTensor S M₁ : (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
              (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
            (LinearMap.inr R M₂ M₃)) :
        M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)))
    LinearMap.id

Tactic:
ext