case h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImageSheaf f ≫ imageSheafι f).val = f.val
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ toImageSheaf f ≫ imageSheafι f = f
ext1
no goals
case h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImageSheaf f ≫ imageSheafι f).val = f.val
simp [toImagePresheafSheafify]