no goals
C : Type u
inst✝⁶ : Category C
inst✝⁵ : HasColimits C
X Y Z : TopCat
inst✝⁴ : ConcreteCategory C
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : ReflectsIsomorphisms (forget C)
F : Sheaf C X
G : Presheaf C X
f : F.val ⟶ G
U : Opens ↑X
h : ∀ (x : { x // x ∈ U }), Function.Injective ((forget C).map ((stalkFunctor C ↑x).map f))
s t : (forget C).obj (F.val.obj U.op)
hst : (forget C).map (f.app U.op) s = (forget C).map (f.app U.op) t
x : { x // x ∈ U }
⊢ (forget C).map ((stalkFunctor C ↑x).map f) ((forget C).map (germ (Sheaf.presheaf F) x) s) =
    (forget C).map ((stalkFunctor C ↑x).map f) ((forget C).map (germ (Sheaf.presheaf F) x) t)
erw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply, hst]