-- 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 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
⊢ Eq.{w + 1} (α :=
    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))))
        (CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X)
          (((Equiv.symm
                    (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                      (↑x1 : Type w) →* (↑x2 : Type w))) :
                  Equiv.{w + 1, v + 1}
                    (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                      (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                    (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
              (HMul.hMul (α :=
                ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                      (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                      (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X))))) ▷
            X)
          (((Equiv.symm
                  (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                    (↑x1 : Type w) →* (↑x2 : Type w))) :
                Equiv.{w + 1, v + 1}
                  (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                  (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
              (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
            (HMul.hMul (α :=
              ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                    (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                    (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) ≫
          CategoryStruct.comp (Y := tensorObj.{v, u_1} (𝒞 := inst) X X)
            (X ◁
              ((Equiv.symm
                      (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                        (↑x1 : Type w) →* (↑x2 : Type w))) :
                    Equiv.{w + 1, v + 1}
                      (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                        (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                      (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                  (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
                (HMul.hMul (α :=
                  ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                    (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                        (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                        (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X))))))
            (((Equiv.symm
                    (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                      (↑x1 : Type w) →* (↑x2 : Type w))) :
                  Equiv.{w + 1, v + 1}
                    (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                      (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                    (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
              (HMul.hMul (α :=
                ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                  (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                      (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                      (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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))))
have a : 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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))) (Y :=
            F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X)))
            (F.map
              (Quiver.Hom.op
                (((Equiv.symm
                          (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                            (↑x1 : Type w) →* (↑x2 : Type w))) :
                        Equiv.{w + 1, v + 1}
                          (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                            MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                          (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                      (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
                    (HMul.hMul (α :=
                      ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                        (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                            (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                            (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X))))) ▷
                  X))) :
          (a : (↑(F.obj (op (X ⊗ X))) : Type w)) → (↑(F.obj (op ((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) 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) X X))))) :
              (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X)))) :
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))) (Y :=
            F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X)))
            (F.map
              (Quiver.Hom.op
                (((Equiv.symm
                          (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                            (↑x1 : Type w) →* (↑x2 : Type w))) :
                        Equiv.{w + 1, v + 1}
                          (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                            MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                          (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                      (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
                    (HMul.hMul (α :=
                      ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
                        (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                            (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                            (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X))))) ▷
                  X))) :
          (a : (↑(F.obj (op (X ⊗ X))) : Type w)) → (↑(F.obj (op ((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) 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) X X))))) :
              (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X)))) :
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w)) =
  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))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorObj.{v, u_1} (𝒞 := inst) X X))))
            (F.map (Quiver.Hom.op (Iso.hom (α_ X X X)))) :
          (a : (↑(F.obj (op (X ⊗ X ⊗ X))) : Type w)) → (↑(F.obj (op ((X ⊗ X) ⊗ X))) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                MonCat.carrier) (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))) (Y :=
                F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                (F.map
                  (Quiver.Hom.op
                    (X ◁
                      ((Equiv.symm
                              (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                                (↑x1 : Type w) →* (↑x2 : Type w))) :
                            Equiv.{w + 1, v + 1}
                              (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                                MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                              (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                          (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
                        (HMul.hMul (α :=
                          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                            MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X)))))))) :
              (a : (↑(F.obj (op (X ⊗ X))) : Type w)) → (↑(F.obj (op (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) 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) X X))))) :
                  (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X)))) :
          (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorObj.{v, u_1} (𝒞 := inst) X X)))) : Type w)) :
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorObj.{v, u_1} (𝒞 := inst) X X))))
            (F.map (Quiver.Hom.op (Iso.hom (α_ X X X)))) :
          (a : (↑(F.obj (op (X ⊗ X ⊗ X))) : Type w)) → (↑(F.obj (op ((X ⊗ X) ⊗ X))) : Type w))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                MonCat.carrier) (X := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))) (Y :=
                F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                (F.map
                  (Quiver.Hom.op
                    (X ◁
                      ((Equiv.symm
                              (α.homEquiv' (CD := MonCat.carrier) (FD := fun (x1 x2 : MonCat.{w}) ↦
                                (↑x1 : Type w) →* (↑x2 : Type w))) :
                            Equiv.{w + 1, v + 1}
                              (ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                                MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X X))))
                              (tensorObj.{v, u_1} (𝒞 := inst) X X ⟶ X)) :
                          (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
                        (HMul.hMul (α :=
                          ToType (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                            MonCat.carrier) (F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) 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) 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) 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) X X))))) :
                                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) 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) 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) X X))))) :
                                (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X)))))))) :
              (a : (↑(F.obj (op (X ⊗ X))) : Type w)) → (↑(F.obj (op (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) 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) X X))))) :
                  (a : X ⊗ X ⟶ X) → ToType (F.obj (op (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) X X)))) :
          (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) X (tensorObj.{v, u_1} (𝒞 := inst) X X)))) : Type w)) :
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorObj.{v, u_1} (𝒞 := inst) X X) X))) : Type w))
Tactic: simp only [α.homEquiv'_comp, Equiv.apply_symm_apply, map_mul]