-- Module: Mathlib.Algebra.Category.CoalgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
X Y Z : CoalgCat R
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))

Tactic:
rfl