-- 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)
rw :
  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)
⊢ 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 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)
    (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:
rw [← yonedaMon_naturality, Category.comp_id, ← Category.id_comp μ[M.X], ← lift_fst_snd]

Premises used: CategoryTheory.yonedaMon_naturality, CategoryTheory.Category.comp_id, CategoryTheory.CartesianMonoidalCategory.lift_fst_snd, CategoryTheory.MonObj.mul, CategoryTheory.Category.id_comp