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

Tactic:
cat_disch