∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {W : C} (fst : W ⟶ X)
  (snd : W ⟶ Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g),
  CategoryTheory.Limits.PullbackCone.mk fst snd eq =
    { pt := W,
      π :=
        {
          app := fun j =>
            Option.casesOn j (CategoryTheory.CategoryStruct.comp fst f) fun j' =>
              CategoryTheory.Limits.WalkingPair.casesOn j' fst snd,
          naturality := ⋯ } }