-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Mon (goal)
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)
e_a :
  Eq (α := unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
    (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
        (lift
          ((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))
          ((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)))
        (fst N.X N.X) :
      unop (op (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))
        (fst N.X N.X) :
      unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
⊢ Eq (α := unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
    (lift
        ((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))
        ((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)) :
      unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ 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 ⟶ tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
have e_a₁ : Eq (α := unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
  (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) N.X N.X)
      (lift
        ((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))
        ((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)))
      (snd N.X N.X) :
    unop (op (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))
      (snd N.X N.X) :
    unop (op (tensorObj.{v, u_1} (𝒞 := inst) M.X M.X)) ⟶ N.X)
Tactic: ext