∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasPullback f f] [inst_2 : CategoryTheory.Limits.HasPushout f.op f.op],
  Function.LeftInverse
    (fun h =>
      (CategoryTheory.Limits.Cofork.ofπ f.op.unop ⋯).isColimitOfIsos
        ((CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop f.op f.op ⋯ ⋯ ⋯) h)
        (CategoryTheory.Limits.Cofork.ofπ f ⋯) (CategoryTheory.Limits.pullbackIsoUnopPushout f f).symm
        (CategoryTheory.Iso.refl (Opposite.unop (Opposite.op X)))
        (CategoryTheory.Iso.refl (CategoryTheory.Limits.Cofork.ofπ f.op.unop ⋯).pt) ⋯ ⋯ ⋯)
    fun h =>
    (CategoryTheory.Limits.Fork.ofι f.op ⋯).isLimitOfIsos
      ((CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp f f ⋯ ⋯ ⋯) h) (CategoryTheory.Limits.Fork.ofι f.op ⋯)
      (CategoryTheory.Iso.refl (Opposite.op X)) (CategoryTheory.Limits.pullbackIsoUnopPushout f f).op.symm
      (CategoryTheory.Iso.refl (CategoryTheory.Limits.Fork.ofι f.op ⋯).pt) ⋯ ⋯ ⋯