-- Mathlib/AlgebraicGeometry/Restrict.lean
lemma stalkIso_inv {X : Scheme.{u}} (U : X.Opens) (x : U) :
    (U.stalkIso x).inv = U.ι.stalkMap x

Proof state:
case h.e'_2.h
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
e_1✝ : ((↑U).presheaf.obj (op W) ⟶ (↑U).presheaf.stalk x) = (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U).presheaf.stalk x)
⊢ (↑U).presheaf.germ W x hxW = Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯

Tactic:
refine (U.toScheme.presheaf.germ_res (homOfLE ?_) _ _).symm

Result:
case h.e'_2.h
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
e_1✝ : ((↑U).presheaf.obj (op W) ⟶ (↑U).presheaf.stalk x) = (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U).presheaf.stalk x)
⊢ (Opens.map (Opens.inclusion' U)).toPrefunctor.1 (unop (op (U.ι ''ᵁ W))) ≤ W

Proof state:
X : Scheme
U : X.Opens
x : ↥U
⊢ 𝟙 ((↑U).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
apply TopCat.Presheaf.stalk_hom_ext

Result:
case ih
X : Scheme
U : X.Opens
x : ↥U
⊢ ∀ (U_1 : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace) (hxU : x ∈ U_1),
    (↑U).presheaf.germ U_1 x hxU ≫ 𝟙 ((↑U).presheaf.stalk x) =
      (↑U).presheaf.germ U_1 x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Proof state:
case h.e'_2.h
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
e_1✝ : ((↑U).presheaf.obj (op W) ⟶ (↑U).presheaf.stalk x) = (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U).presheaf.stalk x)
⊢ (Opens.map (Opens.inclusion' U)).toPrefunctor.1 (unop (op (U.ι ''ᵁ W))) ≤ W

Tactic:
exact (Set.preimage_image_eq _ Subtype.val_injective).le

Result:
no goals

Proof state:
case ih
X : Scheme
U : X.Opens
x : ↥U
⊢ ∀ (U_1 : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace) (hxU : x ∈ U_1),
    (↑U).presheaf.germ U_1 x hxU ≫ 𝟙 ((↑U).presheaf.stalk x) =
      (↑U).presheaf.germ U_1 x hxU ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
intro W hxW

Result:
case ih
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW ≫ 𝟙 ((↑U).presheaf.stalk x) =
    (↑U).presheaf.germ W x hxW ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Proof state:
case ih
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW ≫ 𝟙 ((↑U).presheaf.stalk x) =
    (↑U).presheaf.germ W x hxW ≫ (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Tactic:
simp only [Category.comp_id, U.germ_stalkIso_hom_assoc]

Result:
case ih
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) ↑x ⋯ ≫ Hom.stalkMap U.ι x

Proof state:
X : Scheme
U : X.Opens
x : ↥U
⊢ (U.stalkIso x).inv = Hom.stalkMap U.ι x

Tactic:
rw [← Category.comp_id (U.stalkIso x).inv, Iso.inv_comp_eq]

Result:
X : Scheme
U : X.Opens
x : ↥U
⊢ 𝟙 ((↑U).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x

Proof state:
case ih
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
⊢ (↑U).presheaf.germ W x hxW = X.presheaf.germ (U.ι ''ᵁ W) ↑x ⋯ ≫ Hom.stalkMap U.ι x

Tactic:
convert (Scheme.stalkMap_germ U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm

Result:
case h.e'_2.h
X : Scheme
U : X.Opens
x : ↥U
W : TopologicalSpace.Opens ↑↑(↑U).toPresheafedSpace
hxW : x ∈ W
e_1✝ : ((↑U).presheaf.obj (op W) ⟶ (↑U).presheaf.stalk x) = (X.presheaf.obj (op (U.ι ''ᵁ W)) ⟶ (↑U).presheaf.stalk x)
⊢ (↑U).presheaf.germ W x hxW = Hom.app U.ι (U.ι ''ᵁ W) ≫ (↑U).presheaf.germ (U.ι ⁻¹ᵁ U.ι ''ᵁ W) x ⋯