-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑(↑V : X.Opens) : Set ↥X)
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
this :
  Membership.mem (α := (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (γ :=
    Submodule (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        s :
      (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s' : ↥(I.ideal U)
n : ℕ
hs' :
  HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
          s :
        (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
      ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          (↑(s',
                  Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
            (↑Γ(X, (↑U : X.Opens)) : Type u)) :
        (↑Γ(X, X.basicOpen f) : Type u)) =
    (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
        (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
      (↑(s',
              Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1 :
        (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ (x ∈
      X.basicOpen
        (HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
          ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
              s :
            (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
          ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
              (↑(s',
                      Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                        Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                        ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
                (↑Γ(X, (↑U : X.Opens)) : Type u)) :
            (↑Γ(X, X.basicOpen f) : Type u)))) =
    (x ∈
      X.basicOpen (U := X.basicOpen f)
        ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          (↑(s',
                  Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1 :
            (↑Γ(X, (↑U : X.Opens)) : Type u))))

Tactic:
apply_fun (x ∈ X.basicOpen ·) at hs'

Premises used: Membership.mem, AlgebraicGeometry.Scheme.basicOpen