-- 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' :
  (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))
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 ⋯).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)) ⋯).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)) ⋯).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))

Tactic:
cases n