∀ {A B : GrpCat} (f : A ⟶ B),
  (GrpCat.SurjectiveOfEpiAuxs.tau f) GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity =
    GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.fromCoset ⟨↑(GrpCat.Hom.hom f).range, ⋯⟩