-- 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
a :
  HMul.hMul (α := (↑(F.obj (op X)) : Type w)) (β := (↑(F.obj (op X)) : Type w))
      ((((α.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) → ToType (F.obj (op X)))
            (𝟙 X))⁻¹ :
        ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
          (F.obj (op X)))
      (((α.homEquiv' (CD := GrpCat.carrier) (FD := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) :
              Equiv.{v + 1, w + 1} (X ⟶ X)
                (ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
                  (F.obj (op X)))) :
            (a : X ⟶ X) → ToType (F.obj (op X)))
          (𝟙 X) :
        ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
          (F.obj (op X))) =
    1
⊢ HMul.hMul (α := (↑(F.obj (op X)) : Type w)) (β := (↑(F.obj (op X)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (X := F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) (Y := F.obj (op X))
              (F.map
                (Quiver.Hom.op
                  (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)))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type w)) → (↑(F.obj (op X)) : Type w))
          (((α.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)))) :
        (↑(F.obj (op X)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (X := F.obj (op (tensorObj.{v, u} (𝒞 := inst) X X))) (Y := F.obj (op X))
              (F.map
                (Quiver.Hom.op
                  (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)))) :
            (a : (↑(F.obj (op (X ⊗ X))) : Type w)) → (↑(F.obj (op X)) : Type w))
          (((α.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)))) :
        (↑(F.obj (op X)) : Type w)) =
    1

Tactic:
simp only [← α.homEquiv'_comp, Functor.comp_obj, lift_fst, Equiv.apply_symm_apply, lift_snd]

Premises used: CategoryTheory.Functor.comp_obj, Equiv.apply_symm_apply, CategoryTheory.CartesianMonoidalCategory.lift_snd, CategoryTheory.Functor.RepresentableBy.homEquiv'_comp, CategoryTheory.CartesianMonoidalCategory.lift_fst