-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : (↑Γ(X, U) : Type u)
I : Ideal (↑Γ(X, U) : Type u)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    Membership.mem (α := (↑(X.presheaf.stalk x) : Type u)) (γ := Ideal (↑(X.presheaf.stalk x) : Type u))
      (Ideal.map (F := (↑(X.presheaf.obj (op U)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x h) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          s :
        (↑(X.presheaf.stalk x) : Type u))
this_1 : (x : ↥(Spec Γ(X, U))) → Algebra (↑Γ(X, U) : Type u) (↑(X.presheaf.stalk (hU.fromSpec x)) : Type u) :=
  fun (x : ↥(Spec Γ(X, U))) ↦
    X.presheaf.algebra_section_stalk
      (((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' : (a : ↥(Spec Γ(X, U))) → ↥(↑U : Scheme)) x)
this :
  ∀ (P : Ideal (↑Γ(X, U) : Type u)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP : PrimeSpectrum (↑Γ(X, U) : Type u) })) : Type u) P
refine :
  ∀ (P : Ideal (↑Γ(X, U) : Type u)) [inst : P.IsMaximal],
    Membership.mem (α :=
      (fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
          (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
            Type u))
        P inst)
      (γ :=
      Submodule (↑Γ(X, U) : Type u)
        ((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
            (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
              Type u))
          P inst))
      (Submodule.localized₀ P.primeCompl
        ((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
            (Algebra.linearMap (↑Γ(X, U) : Type u)
                ((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
                    (↑(X.presheaf.stalk
                          (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
                      Type u))
                  P hP) :
              LinearMap (R := (↑Γ(X, U) : Type u)) (RingHom.id (↑Γ(X, U) : Type u)) (↑Γ(X, U) : Type u)
                ((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
                    (↑(X.presheaf.stalk
                          (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
                      Type u))
                  P hP)))
          P inst)
        I)
      (((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
                (Algebra.linearMap (↑Γ(X, U) : Type u)
                    ((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
                        (↑(X.presheaf.stalk
                              (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
                          Type u))
                      P hP) :
                  LinearMap (R := (↑Γ(X, U) : Type u)) (RingHom.id (↑Γ(X, U) : Type u)) (↑Γ(X, U) : Type u)
                    ((fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
                        (↑(X.presheaf.stalk
                              (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
                          Type u))
                      P hP)))
              P inst :
            (a : (↑Γ(X, U) : Type u)) →
              (fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
                  (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ })) : Type u))
                P inst)
          s :
        (fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
            (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
              Type u))
          P inst)
⊢ s ∈ I

Tactic:
refine Submodule.mem_of_localization_maximal
      (fun P hP ↦ X.presheaf.stalk (hU.fromSpec ⟨P, hP.isPrime⟩))
      (fun P hP ↦ Algebra.linearMap _ _) _ _ ?_

Premises used: PrimeSpectrum.mk, Submodule.mem_of_localization_maximal, CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.IsAffineOpen.fromSpec, Algebra.linearMap, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Ideal.IsMaximal.isPrime, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace