no goals
C : Type u
inst✝ : Category C
J₁ J₂ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
hS : IsClosed J₁ S
Z : C
g : Z ⟶ Y
hg : Covers J₁ (Sieve.pullback f S) g
⊢ Covers J₁ S (g ≫ f)
rwa [J₁.covers_iff, Sieve.pullback_comp]