∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.Limits.IsLimit
      ((CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.fst f₁ f₂)
            (CategoryTheory.Limits.pullback.snd f₁ f₂) ⋯).pasteVert
        (CategoryTheory.Limits.PullbackCone.mk
          (CategoryTheory.Limits.pullback.lift
            (CategoryTheory.Limits.pullback.fst f₁
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.snd f₁
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
              (CategoryTheory.Limits.pullback.fst f₃ f₄))
            ⋯)
          (CategoryTheory.Limits.pullback.snd f₁
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
          ⋯)
        ⋯) =
    CategoryTheory.Limits.IsLimit
      (CategoryTheory.Limits.PullbackCone.mk
        (CategoryTheory.Limits.pullback.fst f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        (CategoryTheory.Limits.pullback.snd f₁
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
        ⋯)