case w.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ obj G U
x✝ : Cᵒᵖ
a✝ : F'.obj x✝
⊢ (lift G f hf ≫ ι G).app x✝ a✝ = f.app x✝ a✝
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ obj G U
⊢ lift G f hf ≫ ι G = f
ext
no goals
case w.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
f : F' ⟶ F
hf : ∀ (U : Cᵒᵖ) (x : F'.obj U), f.app U x ∈ obj G U
x✝ : Cᵒᵖ
a✝ : F'.obj x✝
⊢ (lift G f hf ≫ ι G).app x✝ a✝ = f.app x✝ a✝
rfl