-- 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.h
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
⊢ ↑(f ⁻¹ᵁ ⊥) = ↑⊥

Tactic:
simp [Opens.map]

Result:
no goals

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 (𝟙 (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

Tactic:
exact H

Result:
no goals

Proof state:
case h.h₂
X✝ X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ ∃ U V,
    U = ⊤ ∧
      V = Scheme.Hom.opensRange f ∧
        ((∀ [hX : IsReduced X] (s : ↑Γ(X, U)),
            X.basicOpen s = ⊥ →
              ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx)) s = 0) →
          ∀ [hX : IsReduced Y] (s : ↑Γ(Y, V)),
            Y.basicOpen s = ⊥ →
              ∀ (x : ↑↑Y.toPresheafedSpace) (hx : x ∈ V), (ConcreteCategory.hom (Y.sheaf.presheaf.germ V x hx)) s = 0)

Tactic:
refine ⟨f ⁻¹ᵁ f.opensRange, f.opensRange, by ext1; simp, rfl, ?_⟩

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

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 :
  ∀ [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
⊢ (ConcreteCategory.hom (X.sheaf.presheaf.germ U x hx✝)) s = 0

Tactic:
specialize H (X.presheaf.map i.op s)

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

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:
rw [RingHom.map_zero]

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

Tactic:
specialize H (inf_bot_eq _) x hx

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

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

Tactic:
rw [← Scheme.stalkMap_germ_apply f ⟨_, _⟩ 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 (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

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

Tactic:
simp

Result:
no goals