-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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 :
  Membership.mem (γ := Submodule (↑Γ(Y, Y.basicOpen s) : Type u) (↑Γ(Y, Y.basicOpen s) : Type u))
    ((fun (U : (↑Y.affineOpens : Type u)) ↦
        (RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            (CommRingCat.Hom.hom (f.app (↑U : Y.Opens))) :
          Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
      (Y.affineBasicOpen s))
    (IsLocalization.mk' (↑Γ(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)
        ((fun (x : ℕ) ↦ s ^ x) n) ⋯))
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj
        (Opposite.op
          (X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
            ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              s)))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
      CommRingCat.carrier)
      ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        x)
      (X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
        ((CommRingCat.Hom.hom (f.app (↑U : Y.Opens)) :
            (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
          s))
      ⋯)
    0
obtain :
  ∀ (n : ℕ)
    (hn :
      HMul.hMul (β := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
          (HPow.hPow (α := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (f.app (↑U : Y.Opens)) :
                  (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                s :
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            n)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (f.app (↑U : Y.Opens)) :
                (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
              x :
            (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) =
        0),
    ∃ (s_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
      Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) s_1 ∧
        Membership.mem (γ := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u))
          ((fun (U : (↑Y.affineOpens : Type u)) ↦
              (RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                  (CommRingCat.Hom.hom (f.app (↑U : Y.Opens))) :
                Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
            U)
          (s_1 * x)
⊢ ∃ (s_1 : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
    Membership.mem (γ := Submonoid (↑Γ(Y, (↑U : Y.Opens)) : Type u)) (Submonoid.powers s) s_1 ∧
      Membership.mem (γ := Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u))
        ((fun (U : (↑Y.affineOpens : Type u)) ↦
            (RingHom.ker (F := (↑Γ(Y, (↑U : Y.Opens)) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
                (CommRingCat.Hom.hom (f.app (↑U : Y.Opens))) :
              Ideal (↑Γ(Y, (↑U : Y.Opens)) : Type u)))
          U)
        (s_1 * x)

Tactic:
obtain ⟨n, hn⟩ := exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact
        X (U := f ⁻¹ᵁ U) (QuasiCompact.isCompact_preimage (f := f) _ U.1.2 U.2.isCompact)
        (f.app U x) (f.app U s) H

Premises used: AlgebraicGeometry.QuasiCompact.isCompact_preimage, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.app, TopologicalSpace.Opens.is_open', Subtype.val, DFunLike.coe, Subtype.property