-- Module: Mathlib.Algebra.Category.CoalgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
X Y Z : CoalgCat R
h :
  ∀ (x : (↑X.toModuleCat : Type u)) (x_1 : (↑Y.toModuleCat : Type u)) (x_2 : (↑Z.toModuleCat : Type u)),
    Eq (α :=
      (↑(Functor.obj
            (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
              (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
              (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
              (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
              (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
        Type u))
      (((((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X.toModuleCat : Type u)) (N := (↑Y.toModuleCat : Type u)) (P :=
                            (↑X.toModuleCat : Type u) ⊗[R] (↑Y.toModuleCat : Type u)) (Q :=
                            (↑Z.toModuleCat : Type u) →ₗ[R]
                              (↑(Functor.obj
                                    (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                      (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                      fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                      ModuleCat.carrier))
                                    (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                                Type u))
                            (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
                            (TensorProduct.mk R (↑X.toModuleCat : Type u) (↑Y.toModuleCat : Type u))
                            (LinearMap.compr₂ₛₗ (R₄ := R) (M :=
                              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)) (N :=
                              (↑Z.toModuleCat : Type u)) (P :=
                              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u) ⊗[R]
                                (↑Z.toModuleCat : Type u))
                              (Q :=
                              (↑(Functor.obj
                                    (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                      (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                      fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                      ModuleCat.carrier))
                                    (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                                Type u))
                              (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
                              (TensorProduct.mk R
                                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)
                                (↑Z.toModuleCat : Type u))
                              (ModuleCat.Hom.hom
                                (CategoryTheory.Functor.map
                                  (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                    (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                    fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                    fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                    ModuleCat.carrier))
                                  (Iso.hom (α_ X Y Z))))) :
                          (↑X.toModuleCat : Type u) →ₗ[R]
                            (↑Y.toModuleCat : Type u) →ₗ[R]
                              (↑Z.toModuleCat : Type u) →ₗ[R]
                                (↑(Functor.obj
                                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                        fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                        fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                        ModuleCat.carrier))
                                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                        (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                                  Type u)) :
                        (a : (↑X.toModuleCat : Type u)) →
                          (↑Y.toModuleCat : Type u) →ₗ[R]
                            (↑Z.toModuleCat : Type u) →ₗ[R]
                              (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y ⊗ Z)) : Type u))
                      x :
                    (↑Y.toModuleCat : Type u) →ₗ[R]
                      (↑Z.toModuleCat : Type u) →ₗ[R]
                        (↑(Functor.obj
                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                ModuleCat.carrier))
                              (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                          Type u)) :
                  (a : (↑Y.toModuleCat : Type u)) →
                    (↑Z.toModuleCat : Type u) →ₗ[R] (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y ⊗ Z)) : Type u))
                x_1 :
              (↑Z.toModuleCat : Type u) →ₗ[R]
                (↑(Functor.obj
                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                        (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                        (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                  Type u)) :
            (a : (↑Z.toModuleCat : Type u)) → (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y ⊗ Z)) : Type u))
          x_2 :
        (↑(Functor.obj
              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
          Type u))
      (((((((LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X.toModuleCat : Type u)) (N := (↑Y.toModuleCat : Type u)) (P :=
                            (↑X.toModuleCat : Type u) ⊗[R] (↑Y.toModuleCat : Type u)) (Q :=
                            (↑Z.toModuleCat : Type u) →ₗ[R]
                              (↑(Functor.obj
                                    (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                      (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                      fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                      ModuleCat.carrier))
                                    (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                                Type u))
                            (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
                            (TensorProduct.mk R (↑X.toModuleCat : Type u) (↑Y.toModuleCat : Type u))
                            (LinearMap.compr₂ₛₗ (R₄ := R) (M :=
                              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)) (N :=
                              (↑Z.toModuleCat : Type u)) (P :=
                              (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u) ⊗[R]
                                (↑Z.toModuleCat : Type u))
                              (Q :=
                              (↑(Functor.obj
                                    (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                      (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                      fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                      fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                      ModuleCat.carrier))
                                    (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                                Type u))
                              (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
                              (TensorProduct.mk R
                                (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)
                                (↑Z.toModuleCat : Type u))
                              (ModuleCat.Hom.hom
                                ((Iso.symm
                                        (Iso.refl
                                          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                                            (Functor.obj
                                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                                ModuleCat.carrier))
                                              (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y))
                                            (Functor.obj
                                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                                ModuleCat.carrier))
                                              Z))) ≪≫
                                      (Iso.symm
                                          (Iso.refl
                                            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                                              (Functor.obj
                                                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                  fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                                                  (CD := ModuleCat.carrier))
                                                X)
                                              (Functor.obj
                                                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                  fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                                                  (CD := ModuleCat.carrier))
                                                Y))) ⊗ᵢ
                                        Iso.refl
                                          (Functor.obj
                                            (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                              (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                              fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                              fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                              ModuleCat.carrier))
                                            Z))) ≪≫
                                    α_
                                        (Functor.obj
                                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                            fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                            ModuleCat.carrier))
                                          X)
                                        (Functor.obj
                                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                            fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                            ModuleCat.carrier))
                                          Y)
                                        (Functor.obj
                                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                            fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                            fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                            ModuleCat.carrier))
                                          Z) ≪≫
                                      (Iso.refl
                                            (Functor.obj
                                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                                ModuleCat.carrier))
                                              X) ⊗ᵢ
                                          Iso.refl
                                            (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                                              (Functor.obj
                                                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                  fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                                                  (CD := ModuleCat.carrier))
                                                Y)
                                              (Functor.obj
                                                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                  fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                  fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u))
                                                  (CD := ModuleCat.carrier))
                                                Z))) ≪≫
                                        Iso.refl
                                          (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                                            (Functor.obj
                                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                                ModuleCat.carrier))
                                              X)
                                            (Functor.obj
                                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                                ModuleCat.carrier))
                                              (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)))).hom)) :
                          (↑X.toModuleCat : Type u) →ₗ[R]
                            (↑Y.toModuleCat : Type u) →ₗ[R]
                              (↑Z.toModuleCat : Type u) →ₗ[R]
                                (↑(Functor.obj
                                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                        fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                        fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                        ModuleCat.carrier))
                                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                        (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                                  Type u)) :
                        (a : (↑X.toModuleCat : Type u)) →
                          (↑Y.toModuleCat : Type u) →ₗ[R]
                            (↑Z.toModuleCat : Type u) →ₗ[R]
                              (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y ⊗ Z)) : Type u))
                      x :
                    (↑Y.toModuleCat : Type u) →ₗ[R]
                      (↑Z.toModuleCat : Type u) →ₗ[R]
                        (↑(Functor.obj
                              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                                fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                                fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                                ModuleCat.carrier))
                              (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                          Type u)) :
                  (a : (↑Y.toModuleCat : Type u)) →
                    (↑Z.toModuleCat : Type u) →ₗ[R] (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y ⊗ Z)) : Type u))
                x_1 :
              (↑Z.toModuleCat : Type u) →ₗ[R]
                (↑(Functor.obj
                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                        (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                      (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                        (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
                  Type u)) :
            (a : (↑Z.toModuleCat : Type u)) → (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X ⊗ Y ⊗ Z)) : Type u))
          x_2 :
        (↑(Functor.obj
              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
          Type u))
⊢ Eq (α :=
    (↑X.toModuleCat : Type u) →ₗ[R]
      (↑Y.toModuleCat : Type u) →ₗ[R]
        (↑Z.toModuleCat : Type u) →ₗ[R]
          (↑(Functor.obj
                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                  (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
            Type u))
    (LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X.toModuleCat : Type u)) (N := (↑Y.toModuleCat : Type u)) (P :=
        (↑X.toModuleCat : Type u) ⊗[R] (↑Y.toModuleCat : Type u)) (Q :=
        (↑Z.toModuleCat : Type u) →ₗ[R]
          (↑(Functor.obj
                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                  (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
            Type u))
        (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
        (TensorProduct.mk R (↑X.toModuleCat : Type u) (↑Y.toModuleCat : Type u))
        (LinearMap.compr₂ₛₗ (R₄ := R) (M :=
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)) (N :=
          (↑Z.toModuleCat : Type u)) (P :=
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u) ⊗[R] (↑Z.toModuleCat : Type u))
          (Q :=
          (↑(Functor.obj
                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                  (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
            Type u))
          (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
          (TensorProduct.mk R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)
            (↑Z.toModuleCat : Type u))
          (ModuleCat.Hom.hom
            (CategoryTheory.Functor.map
              (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
              (Iso.hom (α_ X Y Z))))) :
      (↑X.toModuleCat : Type u) →ₗ[R]
        (↑Y.toModuleCat : Type u) →ₗ[R]
          (↑Z.toModuleCat : Type u) →ₗ[R]
            (↑(Functor.obj
                  (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                    (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                    (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                    (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
              Type u))
    (LinearMap.compr₂ₛₗ (R₄ := R) (M := (↑X.toModuleCat : Type u)) (N := (↑Y.toModuleCat : Type u)) (P :=
        (↑X.toModuleCat : Type u) ⊗[R] (↑Y.toModuleCat : Type u)) (Q :=
        (↑Z.toModuleCat : Type u) →ₗ[R]
          (↑(Functor.obj
                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                  (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
            Type u))
        (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
        (TensorProduct.mk R (↑X.toModuleCat : Type u) (↑Y.toModuleCat : Type u))
        (LinearMap.compr₂ₛₗ (R₄ := R) (M :=
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)) (N :=
          (↑Z.toModuleCat : Type u)) (P :=
          (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u) ⊗[R] (↑Z.toModuleCat : Type u))
          (Q :=
          (↑(Functor.obj
                (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                  (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                  (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                  (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
            Type u))
          (σ₁₄ := RingHom.id R) (σ₂₄ := RingHom.id R) (σ₃₄ := RingHom.id R)
          (TensorProduct.mk R (↑(MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y).toModuleCat : Type u)
            (↑Z.toModuleCat : Type u))
          (ModuleCat.Hom.hom
            ((Iso.symm
                    (Iso.refl
                      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                        (Functor.obj
                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                            (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                            (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          (MonoidalCategoryStruct.tensorObj (𝒞 := category) X Y))
                        (Functor.obj
                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                            (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                            (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          Z))) ≪≫
                  (Iso.symm
                      (Iso.refl
                        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                          (Functor.obj
                            (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                              (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                              fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                              fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                              ModuleCat.carrier))
                            X)
                          (Functor.obj
                            (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                              (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                              fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                              fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                              ModuleCat.carrier))
                            Y))) ⊗ᵢ
                    Iso.refl
                      (Functor.obj
                        (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                          (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                          (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                          (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                        Z))) ≪≫
                α_
                    (Functor.obj
                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                        (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                      X)
                    (Functor.obj
                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                        (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                      Y)
                    (Functor.obj
                      (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                        (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                        (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                        (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                      Z) ≪≫
                  (Iso.refl
                        (Functor.obj
                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                            (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                            (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          X) ⊗ᵢ
                      Iso.refl
                        (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                          (Functor.obj
                            (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                              (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                              fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                              fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                              ModuleCat.carrier))
                            Y)
                          (Functor.obj
                            (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                              (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC :=
                              fun (X : CoalgCat R) ↦ (↑X.toModuleCat : Type u)) (ModuleCat R) (FD :=
                              fun (x1 x2 : ModuleCat R) ↦ (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD :=
                              ModuleCat.carrier))
                            Z))) ≪≫
                    Iso.refl
                      (MonoidalCategoryStruct.tensorObj (𝒞 := ModuleCat.moduleCategory R)
                        (Functor.obj
                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                            (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                            (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          X)
                        (Functor.obj
                          (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                            (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                            (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                            (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                          (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z)))).hom)) :
      (↑X.toModuleCat : Type u) →ₗ[R]
        (↑Y.toModuleCat : Type u) →ₗ[R]
          (↑Z.toModuleCat : Type u) →ₗ[R]
            (↑(Functor.obj
                  (forget₂ (CoalgCat R) (FC := fun (x1 x2 : CoalgCat R) ↦
                    (↑x1.toModuleCat : Type u) →ₗc[R] (↑x2.toModuleCat : Type u)) (CC := fun (X : CoalgCat R) ↦
                    (↑X.toModuleCat : Type u)) (ModuleCat R) (FD := fun (x1 x2 : ModuleCat R) ↦
                    (↑x1 : Type u) →ₗ[R] (↑x2 : Type u)) (CD := ModuleCat.carrier))
                  (MonoidalCategoryStruct.tensorObj (𝒞 := category) X
                    (MonoidalCategoryStruct.tensorObj (𝒞 := category) Y Z))) :
              Type u))

Tactic:
ext