-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
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
⊢ s ∈ I
have 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry : 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 := sorry })) : Type u))
              P inst)
        s :
      (fun (P : Ideal (↑Γ(X, U) : Type u)) (hP : P.IsMaximal) ↦
          (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := sorry : PrimeSpectrum (↑Γ(X, U) : Type u) })) :
            Type u))
        P inst)
Tactic: refine Submodule.mem_of_localization_maximal
      (fun P hP ↦ X.presheaf.stalk (hU.fromSpec ⟨P, hP.isPrime⟩))
      (fun P hP ↦ Algebra.linearMap _ _) _ _ ?_