-- Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp
Goal:
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : GrpCat.{u}} (f : X ⟶ Y),
    Eq (α := (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj X ⟶ Functor.obj (𝟭 GrpCat) Y)
      ((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).map f ≫
        Iso.hom
          ((fun (A : GrpCat.{u}) ↦
              (MulEquiv.toGrpIso
                  (let __src :
                    (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) ≃
                      (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) :=
                    Equiv.refl (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u);
                  { toEquiv := __src, map_mul' := ⋯ }) :
                (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A ≅ Functor.obj (𝟭 GrpCat) A))
            Y))
      (Iso.hom
          ((fun (A : GrpCat.{u}) ↦
              (MulEquiv.toGrpIso
                  (let __src :
                    (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) ≃
                      (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) :=
                    Equiv.refl (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u);
                  { toEquiv := __src, map_mul' := ⋯ }) :
                (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A ≅ Functor.obj (𝟭 GrpCat) A))
            X) ≫
        CategoryTheory.Functor.map (𝟭 GrpCat) f)
⊢ ∀ {X Y : GrpCat.{u}} (f : X ⟶ Y),
    Eq (α := (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj X ⟶ Functor.obj (𝟭 GrpCat) Y)
      ((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).map f ≫
        Iso.hom
          ((fun (A : GrpCat.{u}) ↦
              (MulEquiv.toGrpIso
                  (let __src :
                    (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) ≃
                      (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) :=
                    Equiv.refl (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u);
                  { toEquiv := __src, map_mul' := ⋯ }) :
                (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A ≅ Functor.obj (𝟭 GrpCat) A))
            Y))
      (Iso.hom
          ((fun (A : GrpCat.{u}) ↦
              (MulEquiv.toGrpIso
                  (let __src :
                    (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) ≃
                      (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u) :=
                    Equiv.refl (↑((GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A) : Type u);
                  { toEquiv := __src, map_mul' := ⋯ }) :
                (GrpTypeEquivalenceGrp.inverse ⋙ GrpTypeEquivalenceGrp.functor).obj A ≅ Functor.obj (𝟭 GrpCat) A))
            X) ≫
        CategoryTheory.Functor.map (𝟭 GrpCat) f)

Tactic:
cat_disch