case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
⊢ ∀ (x : { x // x ∈ basicOpen X f }),
    IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
⊢ IsUnit (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f)
apply isUnit_of_isUnit_germ
case h.mk.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit
    (↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
⊢ ∀ (x : { x // x ∈ basicOpen X f }),
    IsUnit (↑(germ X.presheaf x) (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
rintro ⟨_, ⟨x, (hx : IsUnit _), rfl⟩⟩
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f) =
    ↑(germ X.presheaf x) f
case h.mk.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ IsUnit
    (↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f))
convert hx
no goals
case h.e'_3
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
hx : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑(germ X.presheaf { val := ↑x, property := (_ : ∃ a, a ∈ {x | IsUnit (↑(germ X.presheaf x) f)} ∧ ↑a = ↑x) })
      (↑(X.presheaf.map (homOfLE (_ : basicOpen X f ≤ U)).op) f) =
    ↑(germ X.presheaf x) f
convert X.presheaf.germ_res_apply _ _ _