∀ (X : CategoryTheory.CommGrp (Type u_1)),
  CategoryTheory.CategoryStruct.comp
      (CommGrpTypeEquivalenceCommGrp.functor.map
        ((CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.CommGrp (Type u_1)))).hom.app X))
      ((CategoryTheory.NatIso.ofComponents
              (fun A =>
                (let __src :=
                    Equiv.refl
                      ↑((CommGrpTypeEquivalenceCommGrp.inverse.comp CommGrpTypeEquivalenceCommGrp.functor).obj A);
                  { toEquiv := __src, map_mul' := ⋯ }).toCommGrpIso)
              @commGrpTypeEquivalenceCommGrp._proof_1).hom.app
        (CommGrpTypeEquivalenceCommGrp.functor.obj X)) =
    CategoryTheory.CategoryStruct.id (CommGrpTypeEquivalenceCommGrp.functor.obj X)