-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
/-- If `f : X ⟶ Y` is open, injective, `X` is quasi-compact and `Y` is affine, then `f` is stalkwise
injective if it is injective on global sections. -/
lemma stalkMap_injective_of_isOpenMap_of_injective [CompactSpace X]
    (hfopen : IsOpenMap f.base) (hfinj₁ : Function.Injective f.base)
    (hfinj₂ : Function.Injective (f.appTop)) (x : X) :
    Function.Injective (f.stalkMap x)

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfopen : IsOpenMap ⇑(ConcreteCategory.hom f.base)
hfinj₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↑↑X.toPresheafedSpace
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
res : (i : 𝒰.J) → Γ(X, ⊤) ⟶ Γ(𝒰.obj i, ⊤) := fun i => Scheme.Hom.appTop (𝒰.map i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑(ConcreteCategory.hom f.base) '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.J) → Opens ↑↑(𝒰.obj i).toPresheafedSpace :=
  fun i => (𝒰.obj i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.J), W i ≤ 𝒰.map i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.map i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ fn i * g)) = 0
⊢ ∃ n, ∀ (i : 𝒰.J), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0

Tactic:
refine ⟨Finset.sup Finset.univ fn, fun i ↦ ?_⟩

Result:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfopen : IsOpenMap ⇑(ConcreteCategory.hom f.base)
hfinj₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↑↑X.toPresheafedSpace
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
res : (i : 𝒰.J) → Γ(X, ⊤) ⟶ Γ(𝒰.obj i, ⊤) := fun i => Scheme.Hom.appTop (𝒰.map i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑(ConcreteCategory.hom f.base) '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.J) → Opens ↑↑(𝒰.obj i).toPresheafedSpace :=
  fun i => (𝒰.obj i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.J), W i ≤ 𝒰.map i ⁻¹ᵁ U
h0 : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.map i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
fn : 𝒰.J → ℕ
hfn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ fn i * g)) = 0
i : 𝒰.J
⊢ (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ Finset.univ.sup fn * g)) = 0

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfopen : IsOpenMap ⇑(ConcreteCategory.hom f.base)
hfinj₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↑↑X.toPresheafedSpace
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
res : (i : 𝒰.J) → Γ(X, ⊤) ⟶ Γ(𝒰.obj i, ⊤) := fun i => Scheme.Hom.appTop (𝒰.map i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
s : ↑Γ(Y, ⊤)
hyv : (ConcreteCategory.hom f.base) x ∈ Y.basicOpen s
bsle : Y.basicOpen s ≤ { carrier := ⇑(ConcreteCategory.hom f.base) '' U.carrier, is_open' := ⋯ }
W : (i : 𝒰.J) → Opens ↑↑(𝒰.obj i).toPresheafedSpace :=
  fun i => (𝒰.obj i).basicOpen ((ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s))
hwle : ∀ (i : 𝒰.J), W i ≤ 𝒰.map i ⁻¹ᵁ U
i : 𝒰.J
⊢ (ConcreteCategory.hom ((𝒰.obj i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.map i) U (𝒰.map i ⁻¹ᵁ U) ⋯)) 0) =
    0

Tactic:
simp only [map_zero]

Result:
no goals

Proof state:
X Y : Scheme
inst✝¹ : IsAffine Y
f : X ⟶ Y
inst✝ : CompactSpace ↑↑X.toPresheafedSpace
hfopen : IsOpenMap ⇑(ConcreteCategory.hom f.base)
hfinj₁ : Function.Injective ⇑(ConcreteCategory.hom f.base)
hfinj₂ : Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
x : ↑↑X.toPresheafedSpace
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
res : (i : 𝒰.J) → Γ(X, ⊤) ⟶ Γ(𝒰.obj i, ⊤) := fun i => Scheme.Hom.appTop (𝒰.map i)
g : ↑Γ(Y, ⊤)
h : (ConcreteCategory.hom (X.presheaf.germ (f ⁻¹ᵁ ⊤) x True.intro)) ((ConcreteCategory.hom (Scheme.Hom.app f ⊤)) g) = 0
U : Opens ↑↑X.toRingedSpace.toPresheafedSpace
w : U ⟶ ⊤
hx : x ∈ U
hg : (ConcreteCategory.hom (X.toRingedSpace.presheaf.map w.op)) ((ConcreteCategory.hom φ) g) = 0
⊢ x ∈ U.carrier ∧ (ConcreteCategory.hom f.base) x = (ConcreteCategory.hom f.base) x

Tactic:
simpa

Result:
no goals