case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
left✝ : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
⊢ ↑x ∈ ↑U
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
⊢ basicOpen X f ≤ U
rintro _ ⟨x, _, rfl⟩
no goals
case intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
left✝ : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
⊢ ↑x ∈ ↑U
exact x.2