∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Fork.ext._auto_1),
  (CategoryTheory.Limits.Fork.ext i w).inv = CategoryTheory.Limits.Fork.mkHom i.inv ⋯