-- 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)
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

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

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)) [inst : 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 inst)
        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 inst)
        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.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)

Tactic:
exact H _ _

Result:
no goals

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)) [inst : 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 inst)
        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 inst)
        I

Tactic:
intro P hP

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.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

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
⊢ s ∈ I ↔
    ∀ (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

Tactic:
refine ⟨fun hs x hxU ↦ Ideal.mem_map_of_mem _ hs, fun H ↦ ?_⟩

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
⊢ s ∈ I