C : Type u
inst✝ : Category C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Sieve.pullback f S ∈ sieves J Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J Z
C : Type u
inst✝ : Category C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Covers J S f
Z : C
g : Z ⟶ Y
⊢ Covers J S (g ≫ f)
rw [covers_iff] at h⊢
no goals
C : Type u
inst✝ : Category C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Sieve.pullback f S ∈ sieves J Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J Z
simp [h, Sieve.pullback_comp]