∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S')
  (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f')
  (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.lift
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) i₁)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) i₂) ⋯)
      (CategoryTheory.Limits.pullback.fst f' g') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) i₁