-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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))
⊢ False
have hs'₁ : (x ∈
    X.basicOpen
      (HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).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) sorry).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) sorry).1 :
          (↑Γ(X, (↑U : X.Opens)) : Type u))))
Tactic: apply_fun (x ∈ X.basicOpen ·) at hs'
Cleared hypotheses: hs'