-- 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
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

Tactic:
haveI := isReduced_of_isOpenImmersion f

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
⊢ (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) ((ConcreteCategory.hom f.base) x) ⋯)) s = 0

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 : (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.presheaf.map i.op)) s) = 0
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ V x hx)) ((ConcreteCategory.hom (X.sheaf.presheaf.map i.op)) s) = 0

Tactic:
exact H

Result:
no goals

Proof state:
case h.h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ (∀ [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)),
      Y.basicOpen s = ⊥ →
        ∀ (x : ↑↑Y.toPresheafedSpace) (hx : x ∈ Scheme.Hom.opensRange f),
          (ConcreteCategory.hom (Y.sheaf.presheaf.germ (Scheme.Hom.opensRange f) x hx)) s = 0

Tactic:
rintro H hX s hs _ ⟨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
⊢ (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 (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

Tactic:
rw [← CommRingCat.comp_apply, CategoryTheory.IsIso.hom_inv_id, map_zero] 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 (𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom f.base) 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

Proof state:
case h
X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
    (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Tactic:
intro x hx

Result:
case h
X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

Proof state:
X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
⊢ s = 0

Tactic:
apply TopCat.Presheaf.section_ext X.sheaf U

Result:
case h
X : Scheme
hX : IsReduced X
U : X.Opens
s : ↑Γ(X, U)
hs : X.basicOpen s = ⊥
⊢ ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U),
    (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) 0

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

Tactic:
rw [basicOpen_eq_of_affine', PrimeSpectrum.basicOpen_eq_bot_iff] at hs

Result:
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