-- Module: Mathlib.AlgebraicGeometry.Scheme
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))
rw₃ rw₄ : Eq.{u + 1} (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)) 0 0
⊢ 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))

Tactic:
rw [← hu.mul_right_eq_zero, ← map_mul, hf, map_zero]

Premises used: map_zero, IsUnit.mul_right_eq_zero, map_mul