-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Cartesian.Grp (goal)
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
⊢ Eq.{w + 1} (α :=
    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)))
        (CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X X)
          (lift (𝟙 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 X)))
                    (X ⟶ X)) :
                (a : ToType (F.obj (op X))) → X ⟶ 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))⁻¹))
          (((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))))))) :
      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)))
        (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)) :
      ToType (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier) (F.obj (op X)))
have a : 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)))
            (F.map
              (Quiver.Hom.op
                (lift (𝟙 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 X)))
                          (X ⟶ X)) :
                      (a : ToType (F.obj (op X))) → X ⟶ 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))⁻¹)))) :
          (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)))
            (F.map
              (Quiver.Hom.op
                (lift (𝟙 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 X)))
                          (X ⟶ X)) :
                      (a : ToType (F.obj (op X))) → X ⟶ 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))⁻¹)))) :
          (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, Equiv.apply_symm_apply, map_mul, map_one]