-- Lean 4 proof step from Mathlib.Algebra.Category.CoalgCat.Monoidal (goal)
Goal:
R : Type u
inst : CommRing R
X₁ Y₁ X₂ Y₂ : CoalgCat R
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ 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) =
    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₂)))
have hf : ∀
  (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: ext