case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) 0) ↔ x ∈ ↑⊥
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ RingedSpace.basicOpen (toRingedSpace X) 0 = ⊥
ext x
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U),
    ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ x ∈ ↑(RingedSpace.basicOpen (toRingedSpace X) 0) ↔ x ∈ ↑⊥
simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_image, Set.mem_setOf_eq, Subtype.exists,
  exists_and_right, exists_eq_right, Opens.coe_bot, Set.mem_empty_iff_false,
  iff_false, not_exists]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
⊢ ∀ (x_1 : x ∈ U),
    ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
intros hx
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬IsUnit (↑(Presheaf.germ (toRingedSpace X).toPresheafedSpace.presheaf { val := x, property := (_ : x ∈ U) }) 0)
rw [map_zero, isUnit_zero_iff]
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ ¬0 = 1
change (0 : X.stalk x) ≠ (1 : X.stalk x)
no goals
case h.h
X✝ : LocallyRingedSpace
X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
x : ↑↑(toRingedSpace X).toPresheafedSpace
hx : x ∈ U
⊢ 0 ≠ 1
exact zero_ne_one