-- 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 N O X Y : C
inst_4 : MonObj M
inst_5 : MonObj N
inst_6 : MonObj O
F : Functor.{v, w, u_1, w + 1} Cᵒᵖ MonCat
α :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          MonCat.carrier)).RepresentableBy
    X
⊢ HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
      (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X ⟶ X)
                (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) :
            (a : (X ⊗ X) ⊗ X ⟶ X) → ToType (F.obj (op ((X ⊗ X) ⊗ X))))
          (fst (tensorObj.{v, u_1} (𝒞 := inst) X X) X ≫ fst X X) :
        ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
          (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))
      (HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
        (β := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
        (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X ⟶ X)
                  (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) :
              (a : (X ⊗ X) ⊗ X ⟶ X) → ToType (F.obj (op ((X ⊗ X) ⊗ X))))
            (fst (tensorObj.{v, u_1} (𝒞 := inst) X X) X ≫ snd X X) :
          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))
        (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X ⟶ X)
                  (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) :
              (a : (X ⊗ X) ⊗ X ⟶ X) → ToType (F.obj (op ((X ⊗ X) ⊗ X))))
            (snd (tensorObj.{v, u_1} (𝒞 := inst) X X) X) :
          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) =
    HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
      (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X ⟶ X)
                (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) :
            (a : (X ⊗ X) ⊗ X ⟶ X) → ToType (F.obj (op ((X ⊗ X) ⊗ X))))
          (fst (tensorObj.{v, u_1} (𝒞 := inst) X X) X ≫ fst X X) :
        ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
          (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))
      (HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
        (β := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
        (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X ⟶ X)
                  (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) :
              (a : (X ⊗ X) ⊗ X ⟶ X) → ToType (F.obj (op ((X ⊗ X) ⊗ X))))
            (Iso.hom (α_ X X X) ≫ snd X (tensorObj.{v, u_1} (𝒞 := inst) X X) ≫ fst X X) :
          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))
        (((α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                Equiv.{v + 1, w + 1} (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X ⟶ X)
                  (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))))) :
              (a : (X ⊗ X) ⊗ X ⟶ X) → ToType (F.obj (op ((X ⊗ X) ⊗ X))))
            (Iso.hom (α_ X X X) ≫ snd X (tensorObj.{v, u_1} (𝒞 := inst) X X) ≫ snd X X) :
          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X)))))

Tactic:
simp