no goals
C : Type u_1
inst✝² : Category C
D : Type ?u.741
inst✝¹ : Category D
E : Type ?u.748
inst✝ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
U✝ : C
S✝ : Sieve ((𝟭 C).obj U✝)
h : S✝ ∈ GrothendieckTopology.sieves J ((𝟭 C).obj U✝)
⊢ Sieve.functorPullback (𝟭 C) S✝ ∈ GrothendieckTopology.sieves J U✝
simpa using h