no goals
C : Type u
inst✝² : Category C
inst✝¹ : HasColimits C
X Y Z : TopCat
inst✝ : ConcreteCategory C
F : Presheaf C X
U V : Opens ↑X
x : ↑X
hxU : x ∈ U
hxV : x ∈ V
W : Opens ↑X
hxW : x ∈ W
iWU : W ⟶ U
iWV : W ⟶ V
sU : (forget C).obj (F.obj U.op)
sV : (forget C).obj (F.obj V.op)
ih : (forget C).map (F.map iWU.op) sU = (forget C).map (F.map iWV.op) sV
⊢ (forget C).map (germ F { val := x, property := hxU }) sU = (forget C).map (germ F { val := x, property := hxV }) sV
erw [← F.germ_res iWU ⟨x, hxW⟩, ← F.germ_res iWV ⟨x, hxW⟩, comp_apply, comp_apply, ih]