-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Properties (goal)
Goal:
X : Scheme
inst : IsReduced X
x : ↥X
n : ℕ
U : Opens ↥X
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (X.presheaf.obj (op U))
e :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        (s ^ n) :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
V : Opens ↥X
hxV : x ∈ V
iU iV : V ⟶ U
e' :
  Eq (α := (↑Γ(X, V) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
        s :
      (↑(X.presheaf.obj (op V)) : Type u_1))
    (0 : (↑Γ(X, V) : Type u_1))
eq_zero :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.map iU.op ≫ X.presheaf.germ V x hxV) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
eq_zero₁ :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V x hxV) :
          (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X.presheaf.map iU.op) :
              (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1))
            s :
          (↑(X.presheaf.obj (op V)) : Type u_1)) :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        s :
      (↑(X.presheaf.stalk x) : Type u_1))
    (0 : (↑(X.presheaf.stalk x) : Type u_1))
have eq_zero₂ : Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V x hxV) :
        (a : (↑(X.presheaf.obj (op V)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
      0 :
    (↑(X.presheaf.stalk x) : Type u_1))
  (0 : (↑(X.presheaf.stalk x) : Type u_1))
Tactic: rw [← X.presheaf.germ_res iU x hxV, CommRingCat.comp_apply, e', map_zero]