-- 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
⊢ HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) : Type w)) (β :=
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v, u_1} C (𝒞 := 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) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
            (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ 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 (tensorUnit.{v, u_1} C (𝒞 := inst)))))
                      (tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ X)) :
                  (a : ToType (F.obj (op (𝟙_ C)))) → 𝟙_ C ⟶ X)
                1 ▷
              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) (tensorUnit.{v, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v, u_1} C (𝒞 := 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) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
            (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ 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 (tensorUnit.{v, u_1} C (𝒞 := inst)))))
                      (tensorUnit.{v, u_1} C (𝒞 := inst) ⟶ X)) :
                  (a : ToType (F.obj (op (𝟙_ C)))) → 𝟙_ C ⟶ X)
                1 ▷
              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) (tensorUnit.{v, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v, u_1} C (𝒞 := 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) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
        (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ X))))
      (Iso.hom (λ_ X))
have a : HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) : Type w)) (β :=
    (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) : Type w))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := MonCat.carrier)
            (Y := F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) X)))
            (F.map (Quiver.Hom.op (fst (tensorUnit.{v, u_1} C (𝒞 := inst)) X))) :
          (a : (↑(F.obj (op (𝟙_ C))) : Type w)) → (↑(F.obj (op (𝟙_ C ⊗ X))) : Type w))
        1 :
      (↑(F.obj (op (tensorObj.{v, u_1} (𝒞 := inst) (tensorUnit.{v, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v, u_1} C (𝒞 := 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) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
          (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ X))))
        (snd (tensorUnit.{v, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v, u_1} C (𝒞 := inst)) 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) (tensorUnit.{v, u_1} C (𝒞 := 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) (tensorUnit.{v, u_1} C (𝒞 := inst)) X))))) :
      (a : 𝟙_ C ⊗ X ⟶ X) → ToType (F.obj (op (𝟙_ C ⊗ X))))
    (Iso.hom (λ_ X))
Tactic: simp only [whiskerRight_fst, whiskerRight_snd, α.homEquiv'_comp, Equiv.apply_symm_apply]