-- Mathlib/Geometry/RingedSpace/Basic.lean
theorem isUnit_res_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U)) (x : X) (hx : x ∈ U)
    (h : IsUnit (X.presheaf.germ U x hx f)) :
    ∃ (V : Opens X) (i : V ⟶ U) (_ : x ∈ V), IsUnit (X.presheaf.map i.op f)

Proof state:
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
obtain ⟨W', hxW', i₁, i₂, (heq' : (X.presheaf.map i₁.op) _ = (X.presheaf.map i₂.op) 1)⟩ :=
  X.presheaf.germ_eq x hxW hxW _ _ heq

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.map i₂.op)) 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Proof state:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
⊢ (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1

Tactic:
exact heq

Result:
no goals

Proof state:
case intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
g' : ↑(X.presheaf.stalk x)
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * g' = 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.germ_exist x g'

Result:
case intro.intro.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
heq : (ConcreteCategory.hom (X.presheaf.germ U x hx)) f * (ConcreteCategory.hom (X.presheaf.germ V x hxV)) g = 1
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)