-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ (goal)
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_1 : 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))
    α
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)
mul_comm :
  autoParam
    (Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
      (Iso.hom (β_ 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))))))
      (((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)))))))
    IsCommMonObj.mul_comm._autoParam
mul_comm₁ :
  autoParam
    (Eq.{u_1 + 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))))
      (((α.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))))
          (Iso.hom (β_ 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)))))) :
        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))))
          (((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)))))) :
        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)))))
    IsCommMonObj.mul_comm._autoParam
mul_comm₂ :
  autoParam
    (Eq (α :=
      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))))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              CommMonCat.carrier) (X := F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X)))
              (F.map (Quiver.Hom.op (Iso.hom (β_ X X)))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type u_1)) → (↑(F.obj (op (X ⊗ X))) : Type u_1))
          (((α.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))))
              (((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)))))) :
            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)))) :
        (↑(F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) : Type u_1))
      (((α.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))))
          (((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)))))) :
        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)))))
    IsCommMonObj.mul_comm._autoParam
mul_comm₃ :
  autoParam
    ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
            CommMonCat.carrier) (X := F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X)))
            (F.map (Quiver.Hom.op (Iso.hom (β_ X X)))) :
          (a : (↑(F.obj (op (X ⊗ X))) : Type u_1)) → (↑(F.obj (op (X ⊗ X))) : Type u_1))
        (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))))) =
      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)))))
    IsCommMonObj.mul_comm._autoParam
⊢ autoParam (Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X X ⟶ X) (Iso.hom (β_ X X) ≫ μ) μ)
    IsCommMonObj.mul_comm._autoParam
have mul_comm₄ : autoParam
  (HMul.hMul (α := (↑(F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) : Type u_1)) (β :=
      (↑(F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              CommMonCat.carrier) (X := F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X)))
              (F.map (Quiver.Hom.op (Iso.hom (β_ X X)))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type u_1)) → (↑(F.obj (op (X ⊗ X))) : Type u_1))
          (((α.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)))) :
        (↑(F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CC :=
              CommMonCat.carrier) (X := F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X)))
              (F.map (Quiver.Hom.op (Iso.hom (β_ X X)))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type u_1)) → (↑(F.obj (op (X ⊗ X))) : Type u_1))
          (((α.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)))) :
        (↑(F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) : Type u_1)) =
    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)))))
  IsCommMonObj.mul_comm._autoParam
Tactic: simp_rw [this, ← α.homEquiv'.apply_eq_iff_eq, α.homEquiv'_comp,
    Equiv.apply_symm_apply, map_mul, ← α.homEquiv'_comp, op_tensorObj,
    braiding_hom_fst, braiding_hom_snd, _root_.mul_comm]