no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
A : Type u₃
inst✝ : Category A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ GrothendieckTopology.sieves J U✝
⊢ Sieve.functorPushforward (𝟭 C) S✝ ∈ GrothendieckTopology.sieves J ((𝟭 C).obj U✝)
simpa using hS