∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {pullback : C}
  {p₁ : pullback ⟶ X₁} {p₂ : pullback ⟶ X₂}
  {condition : CategoryTheory.CategoryStruct.comp p₁ f₁ = CategoryTheory.CategoryStruct.comp p₂ f₂}
  {isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁ p₂ condition)} {p : pullback ⟶ S}
  {hp₁ : autoParam (CategoryTheory.CategoryStruct.comp p₁ f₁ = p) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam}
  {pullback_1 : C} {p₁_1 : pullback_1 ⟶ X₁} {p₂_1 : pullback_1 ⟶ X₂}
  {condition_1 : CategoryTheory.CategoryStruct.comp p₁_1 f₁ = CategoryTheory.CategoryStruct.comp p₂_1 f₂}
  {isLimit_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁_1 p₂_1 condition_1)}
  {p_1 : pullback_1 ⟶ S}
  {hp₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp p₁_1 f₁ = p_1) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam},
  { pullback := pullback, p₁ := p₁, p₂ := p₂, condition := condition, isLimit := isLimit, p := p, hp₁ := hp₁ } =
      { pullback := pullback_1, p₁ := p₁_1, p₂ := p₂_1, condition := condition_1, isLimit := isLimit_1, p := p_1,
        hp₁ := hp₁_1 } →
    pullback = pullback_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1 ∧ isLimit ≍ isLimit_1 ∧ p ≍ p_1