-- Mathlib/Geometry/RingedSpace/Basic.lean
/-- If the germ of a section `f` is zero in the stalk at `x`, then `f` is zero on some neighbourhood
around `x`. -/
lemma exists_res_eq_zero_of_germ_eq_zero (U : Opens X) (f : X.presheaf.obj (op U)) (x : U)
    (h : X.presheaf.germ U x.val x.property f = 0) :
    ∃ (V : Opens X) (i : V ⟶ U) (_ : x.1 ∈ V), X.presheaf.map i.op f = 0

Proof state:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
simpa using hv4

Result:
no goals

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
have h1 : X.presheaf.germ U x.val x.property f = X.presheaf.germ U x.val x.property 0 := by simpa

Result:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0

Tactic:
simpa

Result:
no goals

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
obtain ⟨V, hv, i, _, (hv4 : (X.presheaf.map i.op) f = (X.presheaf.map _) 0)⟩ :=
  TopCat.Presheaf.germ_eq X.presheaf x.1 x.2 x.2 f 0 h1

Result:
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Proof state:
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
use V, i, hv

Result:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
V : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0