case mp
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f → IsUnit (↑(germ X.presheaf x) f)

case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
⊢ IsUnit (↑(germ X.presheaf x) f) → ↑x ∈ basicOpen X f
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f ↔ IsUnit (↑(germ X.presheaf x) f)
constructor
case mp.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x✝ x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x✝
⊢ IsUnit (↑(germ X.presheaf x✝) f)
case mp
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
⊢ ↑x ∈ basicOpen X f → IsUnit (↑(germ X.presheaf x) f)
rintro ⟨x, hx, a⟩
case mp.intro.intro.refl
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x
⊢ IsUnit (↑(germ X.presheaf x) f)
case mp.intro.intro
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x✝ x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x✝
⊢ IsUnit (↑(germ X.presheaf x✝) f)
cases Subtype.eq a
no goals
case mp.intro.intro.refl
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
hx : x ∈ {x | IsUnit (↑(germ X.presheaf x) f)}
a : ↑x = ↑x
⊢ IsUnit (↑(germ X.presheaf x) f)
exact hx
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑x ∈ basicOpen X f
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
⊢ IsUnit (↑(germ X.presheaf x) f) → ↑x ∈ basicOpen X f
intro h
no goals
case mpr
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj U.op)
x : { x // x ∈ U }
h : IsUnit (↑(germ X.presheaf x) f)
⊢ ↑x ∈ basicOpen X f
exact ⟨x, h, rfl⟩