∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {S S' X Y : C} (f : S' ⟶ S) {v₁₂ : X ⟶ S} {v₂₂ : Y ⟶ S}
  {g : X ⟶ Y},
  v₁₂ = CategoryTheory.CategoryStruct.comp g v₂₂ →
    ∀ [inst_1 : CategoryTheory.Limits.HasPullback v₁₂ f],
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst v₁₂ f) g) v₂₂ =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd v₁₂ f) f