-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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' :
  (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))))
zero :
  ∀
    (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 ⋯).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) 0) ⋯).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) 0) ⋯).1 :
                (↑Γ(X, (↑U : X.Opens)) : Type u))))),
    x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))
have succ : ∀ (n : ℕ)
  (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 + 1)) 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 + 1)) sorry).1 :
              (↑Γ(X, (↑U : X.Opens)) : Type u))))),
  x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))
Tactic: cases n
Cleared hypotheses: n, hs'