∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f] (s : CategoryTheory.Limits.PullbackCone f g),
  CategoryTheory.CategoryStruct.comp s.snd (CategoryTheory.Limits.pullbackConeOfLeftIso f g).fst = s.fst ∧
    CategoryTheory.CategoryStruct.comp s.snd (CategoryTheory.Limits.pullbackConeOfLeftIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (CategoryTheory.Limits.pullbackConeOfLeftIso f g).pt},
        CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.pullbackConeOfLeftIso f g).fst = s.fst →
          CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.pullbackConeOfLeftIso f g).snd = s.snd → m = s.snd