-- Mathlib/AlgebraicGeometry/Properties.lean
theorem eq_zero_of_basicOpen_eq_bot {X : Scheme} [hX : IsReduced X] {U : X.Opens}
    (s : Γ(X, U)) (hs : X.basicOpen s = ⊥) : s = 0

Proof state:
case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Tactic:
specialize H (f.app _ s) _ x ⟨x, rfl⟩

Result:
case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
H :
  ∀ [hX : IsReduced X] (s : ↑Γ(X, f ⁻¹ᵁ Scheme.Hom.opensRange f)),
    X.basicOpen s = ⊥ →
      ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ f ⁻¹ᵁ Scheme.Hom.opensRange f),
        (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x hx)) s = 0
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
⊢ X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) = ⊥

case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
H :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Proof state:
case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
H :
  (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
      ((ConcreteCategory.hom
          (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ }
            ((ConcreteCategory.hom f.base) x) ⋯))
        s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Tactic:
apply_fun inv <| f.stalkMap x at H

Result:
case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
H :
  (ConcreteCategory.hom (inv (Scheme.Hom.stalkMap f x)))
      ((ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
        ((ConcreteCategory.hom
            (Y.presheaf.germ { carrier := (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ }
              ((ConcreteCategory.hom f.base) x) ⋯))
          s)) =
    (ConcreteCategory.hom (inv (Scheme.Hom.stalkMap f x))) 0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Proof state:
case h.h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
hs : IsNilpotent ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s)
x : ↑↑(Spec R).toPresheafedSpace
hx : x ∈ ⊤
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
replace hs := (hs.map (Scheme.ΓSpecIso R).inv.hom).eq_zero

Result:
case h.h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↑↑(Spec R).toPresheafedSpace
hx : x ∈ ⊤
hs : (CommRingCat.Hom.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s) = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Proof state:
case h.h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↑↑(Spec R).toPresheafedSpace
hx : x ∈ ⊤
hs : (CommRingCat.Hom.hom (Scheme.ΓSpecIso R).inv) ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) s) = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
rw [← CommRingCat.comp_apply, Iso.hom_inv_id, CommRingCat.id_apply] at hs

Result:
case h.h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↑↑(Spec R).toPresheafedSpace
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Proof state:
case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
H :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Tactic:
have H : (X.presheaf.germ _ x _).hom _ = 0 := H

Result:
case h.h₂.intro
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
hX : IsReduced Y
s : ↑Γ(Y, Scheme.Hom.opensRange f)
hs : Y.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
this : IsReduced X
H✝ :
  (ConcreteCategory.hom (X.sheaf.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
H :
  (CommRingCat.Hom.hom (X.presheaf.germ (f ⁻¹ᵁ Scheme.Hom.opensRange f) x ⋯))
      ((ConcreteCategory.hom (Scheme.Hom.app f (Scheme.Hom.opensRange f))) s) =
    0
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Proof state:
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange f = ⊤

Tactic:
ext1

Result:
case h
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange f) = ↑⊤

Proof state:
case h.h₃
X : Scheme
R : CommRingCat
hX : IsReduced (Spec R)
s : ↑Γ(Spec R, ⊤)
x : ↑↑(Spec R).toPresheafedSpace
hx : x ∈ ⊤
hs : s = 0
⊢ (ConcreteCategory.hom ((Spec R).sheaf.presheaf.germ ⊤ x hx)) s = 0

Tactic:
rw [hs, map_zero]

Result:
no goals

Proof state:
case h.h₁.intro.intro.intro
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ →
              ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H :
  X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = ⊥ →
    ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ V),
      (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0

Tactic:
rw [Scheme.basicOpen_res, hs] at H

Result:
case h.h₁.intro.intro.intro
X✝ X : Scheme
U : X.Opens
H✝ :
  ∀ (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V),
        ∃ x,
          ∀ [hX : IsReduced X] (s : ↑Γ(X, V)),
            X.basicOpen s = ⊥ →
              ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ V), (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) s = 0
hX : IsReduced X
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
hx✝ : x ∈ U
V : X.Opens
hx : ↑⟨x, hx✝⟩ ∈ V
i : V ⟶ U
H :
  V ⊓ ⊥ = ⊥ →
    ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ V),
      (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0