no goals
C : Type u
inst✝¹ : Category C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : OpenEmbedding ((CategoryTheory.forget TopCat).map f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ germ X.presheaf
        { val := (CategoryTheory.forget TopCat).map f x,
          property :=
            (_ :
              (CategoryTheory.forget TopCat).map f x ∈
                (IsOpenMap.functor (_ : IsOpenMap ((CategoryTheory.forget TopCat).map f))).obj V) } ≫
      (restrictStalkIso X h x).inv =
    germ (restrict X h).presheaf { val := x, property := hx }
rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]