-- 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:
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 (Limits.colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op { obj := W, property := hxW })))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom
        (Limits.colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op { obj := W, property := hxW })))
      1

Tactic:
erw [map_mul, map_one, show X.presheaf.germ _ x hxW ((X.presheaf.map (U.infLELeft V).op) f) =
  X.presheaf.germ U x hx f from X.presheaf.germ_res_apply (Opens.infLELeft U V) x hxW f,
  show X.presheaf.germ _ x hxW (X.presheaf.map (U.infLERight V).op g) =
  X.presheaf.germ _ x hxV g from X.presheaf.germ_res_apply (Opens.infLERight U V) x hxW g]

Result:
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

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))
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
⊢ ∃ V i, ∃ (_ : x ∈ V), IsUnit ((ConcreteCategory.hom (X.presheaf.map i.op)) f)

Tactic:
replace heq : (X.presheaf.germ _ x hxW) ((X.presheaf.map (U.infLELeft V).op) f *
    (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ _ x hxW) 1 := by
  dsimp [germ]
  erw [map_mul, map_one, show X.presheaf.germ _ x hxW ((X.presheaf.map (U.infLELeft V).op) f) =
    X.presheaf.germ U x hx f from X.presheaf.germ_res_apply (Opens.infLELeft U V) x hxW f,
    show X.presheaf.germ _ x hxW (X.presheaf.map (U.infLERight V).op g) =
    X.presheaf.germ _ x hxV g from X.presheaf.germ_res_apply (Opens.infLERight U V) x hxW g]
  exact heq

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))
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)

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 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

Tactic:
dsimp [germ]

Result:
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 (Limits.colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op { obj := W, property := hxW })))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom
        (Limits.colimit.ι ((OpenNhds.inclusion x).op ⋙ X.presheaf) (op { obj := W, property := hxW })))
      1

Proof state:
case h
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
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (i₁ ≫ U.infLELeft V).op)) f)

Tactic:
simp only [map_mul, map_one] at heq'

Result:
case h
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 i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    1
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (i₁ ≫ U.infLELeft V).op)) f)