-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Scheme (goal)
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        s :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
n : ℕ
hf : s ^ n * f = 0
hu :
  IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
rw :
  HMul.hMul (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) (β := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          (s ^ n) :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          f :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) =
    0
rw₁ :
  Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        (s ^ n * f) :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
rw₂ :
  Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        0 :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
have rw₃ : Eq.{u + 1} (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) 0 0
Tactic: rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]