-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X Y : Scheme
f : X.Hom Y
inst : QuasiCompact f
U_1 U : (↑Y.affineOpens : Type u)
s : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this : IsLocalization.Away s (↑Γ(Y, Y.basicOpen s) : Type u)
x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
n : ℕ
hx :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(Y, Y.basicOpen s) : Type u) x
          (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
            Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n) ⋯)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
rw :
  Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        (HMul.hMul (α := (↑Γ(Y, Y.basicOpen s) : Type u)) (β := (↑Γ(Y, Y.basicOpen s) : Type u))
          ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
              (↑(Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n)
                    ⋯) :
                (↑Γ(Y, (↑U : Y.Opens)) : Type u)) :
            (↑Γ(Y, Y.basicOpen s) : Type u))
          (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(Y, Y.basicOpen s) : Type u) x
              (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n) ⋯) :
            (↑Γ(Y, Y.basicOpen s) : Type u))) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
y : ↥(Submonoid.powers s)
⊢ Eq (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            x :
          (↑Γ(Y, Y.basicOpen s) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    (0 : (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
have rw₁ : HMul.hMul (α := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u)) (β := (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(Y, Y.basicOpen s) : Type u))
            (↑(Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
                  Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n) sorry) :
              (↑Γ(Y, (↑U : Y.Opens)) : Type u)) :
          (↑Γ(Y, Y.basicOpen s) : Type u)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
    ((CommRingCat.Hom.hom (f.app (Y.basicOpen s)) :
          (a : (↑Γ(Y, Y.basicOpen s) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u))
        (IsLocalization.mk' (M := Submonoid.powers s) (↑Γ(Y, Y.basicOpen s) : Type u) x
          (Subtype.mk (p := fun (x : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) ↦
            Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) x) (s ^ n) sorry)) :
      (↑Γ(X, f ⁻¹ᵁ Y.basicOpen s) : Type u)) =
  0
Tactic: rw [← IsLocalization.mk'_spec' (M := .powers s), map_mul, hx, mul_zero]