-- Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction
Goal:
R : CommRingCat
p : PrimeSpectrum (↑R : Type u_1)
x : (↑R : Type u_1)
w :
  Membership.mem (γ := Ideal (↑R : Type u_1))
      (asIdeal
        ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
            (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
              PrimeSpectrum (↑R : Type u_1))
          (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
                C((↑(Spec.topObj R) : Type u_1),
                  (↑(Spec.topObj
                        (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            Presheaf.IsSheaf
                              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                            (structureSheaf (↑R : Type u_1)))
                          (op ⊤))) :
                    Type u_1))) :
              (a : PrimeSpectrum (↑R : Type u_1)) →
                PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
            p)))
      x ↔
    Membership.mem (α := (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1)) (γ :=
      Ideal (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
      (IsLocalRing.maximalIdeal (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structureSheaf (↑R : Type u_1)).presheaf.stalk p) : Type u_1))
          x :
        (↑(stalk (TopCat.Sheaf.presheaf (structureSheaf (↑R : Type u_1))) p) : Type u_1))
⊢ Membership.mem (γ := Ideal (↑R : Type u_1))
      (asIdeal
        ((TopCat.Hom.hom (Spec.topMap (toSpecΓ R)) :
            (a : PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1)) →
              PrimeSpectrum (↑R : Type u_1))
          (((TopCat.Hom.hom (Spec.locallyRingedSpaceObj R).toΓSpecBase :
                C((↑(Spec.topObj R) : Type u_1),
                  (↑(Spec.topObj
                        (Functor.obj (C := (Opens (PrimeSpectrum (↑R : Type u_1)))ᵒᵖ)
                          (ObjectProperty.FullSubcategory.obj (P :=
                            Presheaf.IsSheaf
                              (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑R : Type u_1)) : Type u_1)))
                            (structureSheaf (↑R : Type u_1)))
                          (op ⊤))) :
                    Type u_1))) :
              (a : PrimeSpectrum (↑R : Type u_1)) →
                PrimeSpectrum (↑((structureSheaf (↑R : Type u_1)).obj.obj (op ⊤)) : Type u_1))
            p)))
      x ↔
    x ∈ p.asIdeal

Tactic:
rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff ((structureSheaf R).presheaf.stalk p)
        p.asIdeal x]

Premises used: CommRingCat.carrier, IsLocalization.AtPrime.to_map_mem_maximal_iff, TopCat.Presheaf.stalk, IsLocalization.AtPrime.isLocalRing, AlgebraicGeometry.Spec.structureSheaf, TopCat.Sheaf.presheaf, PrimeSpectrum.asIdeal