-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem restrictStalkIso_inv_eq_ofRestrict {U : TopCat} (X : PresheafedSpace.{_, _, v} C)
    {f : U ⟶ (X : TopCat.{v})} (h : IsOpenEmbedding f) (x : U) :
    (X.restrictStalkIso h x).inv = (X.ofRestrict h).stalkMap x

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (X.restrict h).presheaf)
            ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)) ≫
          (X.restrictStalkIso h x).hom

Tactic:
erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf)
    (h.isOpenMap.functorNhds x).op]

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((⋯.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    X.presheaf.map
        ((⋯.adjunction.counit.app
              (unop ((OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op.obj (op V)))).op ≫
          ⋯.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫
      colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
        ((⋯.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Tactic:
exact (colimit.w ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf) i.op).symm

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((⋯.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Tactic:
erw [← X.presheaf.map_comp_assoc]

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    X.presheaf.map
        ((⋯.adjunction.counit.app
              (unop ((OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op.obj (op V)))).op ≫
          ⋯.functor.op.map ((NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv).app (op V))) ≫
      colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
        ((⋯.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x

Tactic:
let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
  homOfLE (Set.image_preimage_subset f _)

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (⋯.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x