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

Tactic:
choose fn hfn using h1

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
⊢ ∃ n, ∀ (i : 𝒰.J), (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))
hwle : ∀ (i : 𝒰.J), W i ≤ 𝒰.map i ⁻¹ᵁ U
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) g = 0

Tactic:
have h0 (i : 𝒰.J) : (𝒰.map i).appLE _ (W i) (by simp) (φ g) = 0 := by
  rw [← Scheme.Hom.appLE_map _ _ (homOfLE <| hwle i).op, ← Scheme.Hom.map_appLE _ le_rfl w.op]
  simp only [CommRingCat.comp_apply]
  rw [hg]
  simp only [map_zero]

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
h0 : ∀ (i : 𝒰.J), (ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.map i) ⊤ (W i) ⋯)) ((ConcreteCategory.hom φ) g) = 0
⊢ (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)
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
refine stalkMap_injective_of_isAffine _ _ (fun (g : Γ(Y, ⊤)) 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 (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