-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Opens ↥Y
hU : IsAffineOpen U
x : ↥X
hx : Membership.mem (α := ↥Y) U (f x : ↥Y)
h :
  ∀ (g : (↑(Y.presheaf.obj (op U)) : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
                  (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
                g :
              (↑(Y.presheaf.stalk (f x)) : Type u)) :
          (↑(X.presheaf.stalk x) : Type u))
        (0 : (↑(X.presheaf.stalk x) : Type u)) →
      Eq (α := (↑(Y.presheaf.stalk (f x)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            g :
          (↑(Y.presheaf.stalk (f x)) : Type u))
        (0 : (↑(Y.presheaf.stalk (f x)) : Type u))
this : Algebra (↑(Y.presheaf.obj (op U)) : Type u)
  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :=
  Y.presheaf.algebra_section_stalk (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx)
⊢ Function.Injective (α := (↑(Y.presheaf.stalk (f x)) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
have h₁ : ∀ (x_1 : (↑Γ(Y, U) : Type u)),
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
            (a : (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          ((algebraMap (↑Γ(Y, U) : Type u)
                  (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :
                (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u))
              x_1 :
            (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u)) :
        (↑(X.presheaf.stalk x) : Type u))
      (0 : (↑(X.presheaf.stalk x) : Type u)) →
    Eq (α := (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
      ((algebraMap (↑Γ(Y, U) : Type u)
              (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u) :
            (a : (↑Γ(Y, U) : Type u)) → (↑(Y.presheaf.stalk (↑⟨f x, hx⟩ : ↥Y)) : Type u))
          x_1 :
        (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
      (0 : (↑(Y.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) hx) : ↥Y)) : Type u))
Tactic: apply (hU.isLocalization_stalk ⟨f x, hx⟩).injective_of_map_algebraMap_zero