-- 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
P : Ideal (↑Γ(X, U) : Type u)
hP : 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 hP)
    (γ :=
    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 hP))
    (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 hP)
      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 hP :
          (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 hP)
        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 hP)
have rw : 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 hP)
  (γ :=
  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 hP))
  (Submodule.restrictScalars (↑Γ(X, U) : Type u)
    (Ideal.map (F :=
      (↑Γ(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)
      (algebraMap (↑Γ(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))
      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 hP :
        (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 hP)
      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 hP)
Tactic: rw [Ideal.localized₀_eq_restrictScalars_map]