∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X₃ Y₁ Y₂ Y₃ : C} {g₁ : Y₁ ⟶ Y₂} {g₂ : Y₂ ⟶ Y₃}
  {i₃ : X₃ ⟶ Y₃} {t₂ : CategoryTheory.Limits.PullbackCone g₂ i₃} {i₂ : t₂.pt ⟶ Y₂}
  {t₁ : CategoryTheory.Limits.PullbackCone g₁ i₂} (hi₂ : i₂ = t₂.fst)
  (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp g₁ g₂) i₃) (l₁ : s.pt ⟶ t₁.pt),
  CategoryTheory.CategoryStruct.comp l₁ t₁.fst = s.fst →
    ∀ {m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt},
      CategoryTheory.CategoryStruct.comp m (t₂.pasteHoriz t₁ hi₂).fst = s.fst →
        CategoryTheory.CategoryStruct.comp m t₁.fst = CategoryTheory.CategoryStruct.comp l₁ t₁.fst