-- Module: Mathlib.Algebra.Category.CoalgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
X₁ Y₁ X₂ Y₂ : CoalgCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
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) X₁ X₂)) :
    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) Y₁ Y₂)) :
      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))
              (f ⊗ₘ g)) :
          (a : (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁ ⊗ X₂)) : Type u)) →
            (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (Y₁ ⊗ Y₂)) : Type u))
        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₁ Y₂)) :
        Type u))
    ((ModuleCat.Hom.hom
            (Iso.inv
                (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))
                      X₂))) ≫
              (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))
                    f ⊗ₘ
                  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))
                    g) ≫
                Iso.hom
                  (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))
                        Y₂)))) :
          (a : (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (X₁ ⊗ X₂)) : Type u)) →
            (↑((forget₂ (CoalgCat R) (ModuleCat R)).obj (Y₁ ⊗ Y₂)) : Type u))
        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₁ Y₂)) :
        Type u))

Tactic:
rfl