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

Tactic:
obtain ⟨_, ⟨s, rfl⟩, hyv, bsle⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_basicOpen Y)
  (show f.base x ∈ ⟨f.base '' U.carrier, hfopen U.carrier U.is_open'⟩ from ⟨x, by simpa⟩)

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

Proof state:
case intro.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
h1 : ∀ (i : 𝒰.J), ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
n : ℕ
hn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
⊢ (ConcreteCategory.hom (Y.presheaf.Γgerm ((ConcreteCategory.hom f.base) x))) g = 0

Tactic:
apply germ_eq_zero_of_pow_mul_eq_zero (U := ⊤) ⟨f.base x, trivial⟩ hyv

Result:
case intro.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
h1 : ∀ (i : 𝒰.J), ∃ n, (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
n : ℕ
hn : ∀ (i : 𝒰.J), (ConcreteCategory.hom (res i)) ((ConcreteCategory.hom φ) (s ^ n * g)) = 0
⊢ s ^ ?m.58328 * g = 0

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