-- 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
i : 𝒰.J
⊢ ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0

Tactic:
obtain ⟨n, hn⟩ := exists_of_res_zero_of_qcqs_of_top (s := ((res i) (φ s))) (h0 i)

Result:
case intro
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
i : 𝒰.J
n : ℕ
hn :
  (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) s) ^ n *
      (Scheme.Hom.app (𝒰.map i) ⊤).hom' ((ConcreteCategory.hom φ) g) =
    0
⊢ ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0

Proof state:
case intro.intro.intro.intro.intro.intro.intro
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))
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) g = 0

Tactic:
have hwle (i : 𝒰.J) : W i ≤ (𝒰.map i)⁻¹ᵁ U := by
  show (𝒰.obj i).basicOpen ((𝒰.map i ≫ f).appTop s) ≤ _
  rw [← Scheme.preimage_basicOpen_top, Scheme.comp_coeBase, Opens.map_comp_obj]
  refine Scheme.Hom.preimage_le_preimage_of_le _
    (le_trans (f.preimage_le_preimage_of_le bsle) (le_of_eq ?_))
  simp [Set.preimage_image_eq _ hfinj₁]

Result:
case intro.intro.intro.intro.intro.intro.intro
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
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) 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 (Scheme.Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) g) =
    0
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) g = 0

Tactic:
rw [TopCat.Presheaf.Γgerm, Scheme.stalkMap_germ_apply] at h

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
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) g = 0