∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y : C} (f : Y ⟶ X)
  (Hf : CategoryTheory.EffectiveEpiStruct f)
  (S : CategoryTheory.Limits.Cocone (CategoryTheory.Sieve.generateSingleton f).arrows.diagram)
  (j : (CategoryTheory.Sieve.generateSingleton f).arrows.category),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Sieve.generateSingleton f).arrows.cocone.ι.app j)
      (Hf.desc (S.ι.app { obj := CategoryTheory.Over.mk f, property := ⋯ }) ⋯) =
    S.ι.app j