-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X : C
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ CommMonCat
α :
  (F ⋙
        forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
          CommMonCat.carrier)).RepresentableBy
    X
this : MonObj X :=
  MonObj.ofRepresentableBy.{u_1, v, u} X
    (F ⋙
      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
        CommMonCat.carrier) MonCat (FD := fun (x1 x2 : MonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
        MonCat.carrier))
    α
⊢ IsCommMonObj.{v, u} X
have this₁ : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (μ : tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
  (((Equiv.symm
            (α.homEquiv' (CD := CommMonCat.carrier) (FD := fun (x1 x2 : CommMonCat.{u_1}) ↦
              (↑x1 : Type u_1) →* (↑x2 : Type u_1))) :
          Equiv.{u_1 + 1, v + 1}
            (ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              CommMonCat.carrier) (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
            (tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)) :
        (a : ToType (F.obj (op (X ⊗ X)))) → X ⊗ X ⟶ X)
      (HMul.hMul (α :=
        ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := CommMonCat.carrier)
          (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
        (β :=
        ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC := CommMonCat.carrier)
          (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
        (((α.homEquiv' (CD := CommMonCat.carrier) (FD := fun (x1 x2 : CommMonCat.{u_1}) ↦
                  (↑x1 : Type u_1) →* (↑x2 : Type u_1)) :
                Equiv.{v + 1, u_1 + 1} (tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
                  (ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
                    CommMonCat.carrier) (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))) :
              (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
            (fst X X) :
          ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            CommMonCat.carrier) (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
        (((α.homEquiv' (CD := CommMonCat.carrier) (FD := fun (x1 x2 : CommMonCat.{u_1}) ↦
                  (↑x1 : Type u_1) →* (↑x2 : Type u_1)) :
                Equiv.{v + 1, u_1 + 1} (tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
                  (ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
                    CommMonCat.carrier) (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))) :
              (a : X ⊗ X ⟶ X) → ToType (F.obj (op (X ⊗ X))))
            (snd X X) :
          ToType (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            CommMonCat.carrier) (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))) :
    tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
Tactic: have : μ = α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) := rfl