-- 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
i : 𝒰.J
⊢ (ConcreteCategory.hom ((𝒰.obj i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.map i) U (𝒰.map i ⁻¹ᵁ U) ⋯))
        ((ConcreteCategory.hom (X.presheaf.map w.op)) ((ConcreteCategory.hom φ) g))) =
    0

Tactic:
rw [hg]

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
i : 𝒰.J
⊢ (ConcreteCategory.hom ((𝒰.obj i).presheaf.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (Scheme.Hom.appLE (𝒰.map i) U (𝒰.map i ⁻¹ᵁ U) ⋯)) 0) =
    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))
i : 𝒰.J
⊢ (Opens.map (𝒰.map i).base).obj ((Opens.map f.base).obj (Y.basicOpen s)) ≤ 𝒰.map i ⁻¹ᵁ U

Tactic:
refine Scheme.Hom.preimage_le_preimage_of_le _
  (le_trans (f.preimage_le_preimage_of_le bsle) (le_of_eq ?_))

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))
i : 𝒰.J
⊢ f ⁻¹ᵁ { carrier := ⇑(ConcreteCategory.hom f.base) '' U.carrier, is_open' := ⋯ } = U