-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v, u_1} C
inst_1 : CartesianMonoidalCategory.{v, u_1} C
inst_2 : Category.{w, u_2} D
inst_3 : CartesianMonoidalCategory.{w, u_2} D
M_1 N_1 O X Y : C
inst_4 : MonObj M_1
inst_5 : MonObj N_1
inst_6 : MonObj O
M N : Mon.{v, u_1} C
α : Quiver.Hom (V := Functor.{v, v, u_1, v + 1} Cᵒᵖ MonCat) (yonedaMonObj M.X) (yonedaMonObj N.X)
refine :
  HMul.hMul (α := (↑(Functor.obj (yonedaMonObj N.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) : Type v)) (β :=
      (↑(Functor.obj (yonedaMonObj N.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) : Type v))
      ((MonCat.Hom.hom (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
            (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
              (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
          (fst M.X M.X) :
        (↑(Functor.obj (yonedaMonObj N.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) : Type v))
      ((MonCat.Hom.hom (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
            (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
              (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
          (snd M.X M.X) :
        (↑(Functor.obj (yonedaMonObj N.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) : Type v)) =
    CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
          (𝟙 M.X) ⊗ₘ
        (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
              (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
            (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
          (𝟙 M.X))
      μ
⊢ Eq (α := tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC := MonCat.carrier)
            (X := Functor.obj (yonedaMonObj M.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)))
            (α.app (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) :
          (a : (↑((yonedaMonObj M.X).obj (op (M.X ⊗ M.X))) : Type v)) →
            (↑((yonedaMonObj N.X).obj (op (M.X ⊗ M.X))) : Type v))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) M.X M.X) (lift (fst M.X M.X) (snd M.X M.X)) μ) :
      (↑(Functor.obj (yonedaMonObj N.X) (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X))) : Type v))
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X) ⊗ₘ
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{v}) ↦ (↑x1 : Type v) →* (↑x2 : Type v)) (CC :=
                MonCat.carrier) (X := Functor.obj (yonedaMonObj M.X) (op M.X)) (α.app (op M.X)) :
              (a : (↑((yonedaMonObj M.X).obj (op M.X)) : Type v)) → (↑((yonedaMonObj N.X).obj (op M.X)) : Type v))
            (𝟙 M.X))
        μ :
      tensorObj.{v, u_1} (𝒞 := inst) M.X M.X ⟶ N.X)

Tactic:
refine ((α.app _).hom.map_mul _ _).trans ?_

Premises used: MonCat.Hom.hom, MonoidHom.map_mul, CategoryTheory.NatTrans.app, Eq.trans