∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (f : Y ⟶ h.pullback)
  (f_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam)
  (f_p₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam)
  (f_p :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam)
  (f_1 : Y ⟶ h.pullback)
  (f_p₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam)
  (f_p₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam)
  (f_p_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam),
  ({ f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p } = { f := f_1, f_p₁ := f_p₁_1, f_p₂ := f_p₂_1, f_p := f_p_1 }) =
    (f = f_1)