∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π),
  CategoryTheory.CategoryStruct.comp self.rightSection π = CategoryTheory.CategoryStruct.id Z