no goals
C : Type u_3
inst✝² : Category C
D : Type u_4
inst✝¹ : Category D
E : Type ?u.4289
inst✝ : Category E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
X : D
Y : C
f : G.obj Y ⟶ X
⊢ 𝟙 (G.obj Y) ≫ f = f
simp