∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.pullback f (S ⊓ R) = CategoryTheory.Sieve.pullback f S ⊓ CategoryTheory.Sieve.pullback f R