-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma mem_ideal_iff {s : Γ(X, U)} {I : Ideal Γ(X, U)} :
    s ∈ I ↔ ∀ (x : X) (h : x ∈ U), X.presheaf.germ U x h s ∈ I.map (X.presheaf.germ U x h).hom

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
⊢ s ∈ I

Tactic:
have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalization.AtPrime _ P :=
    hU.isLocalization_stalk' ⟨P, hP⟩ (hU.isoSpec.inv.base _).2

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP }))) P
⊢ s ∈ I

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝¹ : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
this✝ :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP }))) P
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalizedModule P.primeCompl
      (Algebra.linearMap ↑Γ(X, U)
        ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP })))
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ ((fun P hP =>
          Algebra.linearMap (↑Γ(X, U))
            ((fun P hP => ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := ⋯ })))
              P hP))
        P hP)
      s ∈
    Submodule.localized₀ P.primeCompl
      ((fun P hP =>
          Algebra.linearMap (↑Γ(X, U))
            ((fun P hP => ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := ⋯ })))
              P hP))
        P hP)
      I

Tactic:
rw [Ideal.localized₀_eq_restrictScalars_map]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝¹ : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
this✝ :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP }))) P
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalizedModule P.primeCompl
      (Algebra.linearMap ↑Γ(X, U)
        ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP })))
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ ((fun P hP =>
          Algebra.linearMap (↑Γ(X, U))
            ((fun P hP => ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := ⋯ })))
              P hP))
        P hP)
      s ∈
    Submodule.restrictScalars (↑Γ(X, U))
      (Ideal.map
        (algebraMap (↑Γ(X, U))
          ((fun P hP => ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := ⋯ }))) P
            hP))
        I)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
⊢ s ∈ I

Tactic:
letI (x) : Algebra Γ(X, U) (X.presheaf.stalk (hU.fromSpec.base x)) :=
  TopCat.Presheaf.algebra_section_stalk X.presheaf _

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
⊢ s ∈ I

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP }))) P
⊢ s ∈ I

Tactic:
have (P : Ideal Γ(X, U)) [hP : P.IsPrime] : IsLocalizedModule P.primeCompl _ :=
  (@isLocalizedModule_iff_isLocalization' ..).mpr (this P)

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↑↑X.toPresheafedSpace) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝¹ : (x : ↑↑(Spec Γ(X, U)).toPresheafedSpace) →
  Algebra ↑Γ(X, U) ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) x)) :=
  fun x =>
    X.presheaf.algebra_section_stalk ((LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom hU.isoSpec.inv)).base.hom' x)
this✝ :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime
      (↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP }))) P
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalizedModule P.primeCompl
      (Algebra.linearMap ↑Γ(X, U)
        ↑(X.presheaf.stalk ((ConcreteCategory.hom hU.fromSpec.base) { asIdeal := P, isPrime := hP })))
⊢ s ∈ I