-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma stalkMap_injective (f : X ⟶ Y) {U : Opens Y} (hU : IsAffineOpen U) (x : X)
    (hx : f.base x ∈ U)
    (h : ∀ g, f.stalkMap x (Y.presheaf.germ U (f.base x) hx g) = 0 →
      Y.presheaf.germ U (f.base x) hx g = 0) :
    Function.Injective (f.stalkMap x)

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
U : Opens ↑↑Y.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g) =
        0 →
      (ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩) :=
  Y.presheaf.algebra_section_stalk ⟨(ConcreteCategory.hom f.base) x, hx⟩
⊢ ∀ (x_1 : ↑Γ(Y, U)),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩)) x_1) =
        0 →
      (algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩)) x_1 = 0

Tactic:
exact h

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Opens ↑↑Y.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g) =
        0 →
      (ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g = 0
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
letI := Y.presheaf.algebra_section_stalk ⟨f.base x, hx⟩

Result:
X Y : Scheme
f : X ⟶ Y
U : Opens ↑↑Y.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g) =
        0 →
      (ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩) :=
  Y.presheaf.algebra_section_stalk ⟨(ConcreteCategory.hom f.base) x, hx⟩
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Proof state:
X Y : Scheme
f : X ⟶ Y
U : Opens ↑↑Y.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g) =
        0 →
      (ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩) :=
  Y.presheaf.algebra_section_stalk ⟨(ConcreteCategory.hom f.base) x, hx⟩
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.stalkMap f x))

Tactic:
apply (hU.isLocalization_stalk ⟨f.base x, hx⟩).injective_of_map_algebraMap_zero

Result:
case h
X Y : Scheme
f : X ⟶ Y
U : Opens ↑↑Y.toPresheafedSpace
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : (ConcreteCategory.hom f.base) x ∈ U
h :
  ∀ (g : ↑(Y.presheaf.obj (op U))),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g) =
        0 →
      (ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hx)) g = 0
this : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩) :=
  Y.presheaf.algebra_section_stalk ⟨(ConcreteCategory.hom f.base) x, hx⟩
⊢ ∀ (x_1 : ↑Γ(Y, U)),
    (ConcreteCategory.hom (Scheme.Hom.stalkMap f x))
          ((algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩)) x_1) =
        0 →
      (algebraMap ↑Γ(Y, U) ↑(Y.presheaf.stalk ↑⟨(ConcreteCategory.hom f.base) x, hx⟩)) x_1 = 0