no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S✝ R✝ : Sieve X
f : Y ⟶ X
S R : Sieve X
⊢ pullback f (S ⊓ R) = pullback f S ⊓ pullback f R
simp [Sieve.ext_iff]