-- Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : CartesianMonoidalCategory.{v, u} C
M G H X Y : C
inst_2 : MonObj M
inst_3 : GrpObj G
inst_4 : GrpObj H
F : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
α :
  (F ⋙
        forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
          GrpCat.carrier)).RepresentableBy
    X
change :
  Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X)
        (lift
          (((Equiv.symm
                  (α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦
                    (↑x1 : Type w) →* (↑x2 : Type w))) :
                Equiv.{w + 1, v + 1}
                  (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                    (F.obj (op X)))
                  (X ⟶ X)) :
              (a : ToType (F.obj (op X))) → X ⟶ X)
            (((α.homEquiv :
                    Equiv.{v + 1, w + 1} (X ⟶ X)
                      ((F ⋙
                            forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                              GrpCat.carrier)).obj
                        (op X))) :
                  (a : X ⟶ X) → (F ⋙ forget GrpCat).obj (op X))
                (𝟙 X))⁻¹)
          (𝟙 X))
        (((Equiv.symm
                (α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦
                  (↑x1 : Type w) →* (↑x2 : Type w))) :
              Equiv.{w + 1, v + 1}
                (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.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 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
            (β :=
            ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
            (((α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                    Equiv.{v + 1, w + 1} (tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
                      (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.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 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))))
            (((α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
                    Equiv.{v + 1, w + 1} (tensorObj.{v, u} (𝒞 := inst) X X ⟶ X)
                      (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.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 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                (F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X)))))) :
      X ⟶ X)
    (CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X)
        (((Equiv.symm
                (α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦
                  (↑x1 : Type w) →* (↑x2 : Type w))) :
              Equiv.{w + 1, v + 1}
                (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                  (F.obj (op (tensorUnit.{v, u} C (𝒞 := inst)))))
                (tensorUnit.{v, u} C (𝒞 := inst) ⟶ X)) :
            (a : ToType (F.obj (op (𝟙_ C)))) → 𝟙_ C ⟶ X)
          1) :
      X ⟶ X)
⊢ Eq.{v + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X)
        (lift
          (((Equiv.symm
                  (α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦
                    (↑x1 : Type w) →* (↑x2 : Type w))) :
                Equiv.{w + 1, v + 1}
                  (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                    (F.obj (op X)))
                  (X ⟶ X)) :
              (a : ToType (F.obj (op X))) → X ⟶ X)
            (((α.homEquiv :
                    Equiv.{v + 1, w + 1} (X ⟶ X)
                      ((F ⋙
                            forget GrpCat (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC :=
                              GrpCat.carrier)).obj
                        (op X))) :
                  (a : X ⟶ X) → (F ⋙ forget GrpCat).obj (op X))
                (𝟙 X))⁻¹)
          (𝟙 X))
        μ :
      X ⟶ X)
    (CategoryStruct.comp (Y := tensorUnit.{v, u} C (𝒞 := inst)) (toUnit X) η : X ⟶ X)

Tactic:
change lift (α.homEquiv'.symm (α.homEquiv (𝟙 X))⁻¹) (𝟙 X) ≫
      α.homEquiv'.symm (α.homEquiv' (fst X X) * α.homEquiv' (snd X X)) =
        toUnit X ≫ α.homEquiv'.symm 1

Premises used: HMul.hMul, CategoryTheory.Functor.RepresentableBy.homEquiv', CategoryTheory.CategoryStruct.id, CategoryTheory.SemiCartesianMonoidalCategory.snd, CategoryTheory.CartesianMonoidalCategory.lift, Inv.inv, Equiv.symm, OfNat.ofNat, CategoryTheory.Functor.RepresentableBy.homEquiv, DFunLike.coe, CategoryTheory.SemiCartesianMonoidalCategory.toUnit, CategoryTheory.SemiCartesianMonoidalCategory.fst