-- Module: Mathlib.AlgebraicGeometry.AffineScheme
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)
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))
⊢ 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))

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

Premises used: IsLocalization.injective_of_map_algebraMap_zero