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
g : Z ⟶ Y
S : Sieve X
⊢ pullback (g ≫ f) S = pullback g (pullback f S)
simp [Sieve.ext_iff]