-- Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
obtain :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)),
    ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
obtain₁ :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl)),
    ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
refine_1 :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl)),
    r ∉ p
refine_2 :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl)),
    IsIdempotentElem r
refine_3 :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl))
    (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
refine_2₁ :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl)),
    IsIdempotentElem r
refine_3₁ refine_3₂ :
  ∀ (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
            { asIdeal := p, isPrime := ⋯ } 1 :
          (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl))
    (this :
      Eq (α := Localization (M := R) p.primeCompl)
        ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
          Localization (M := R) p.primeCompl)
        (1 : Localization (M := R) p.primeCompl))
    (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q

Tactic:
classical
  obtain ⟨r, hr⟩ := PrimeSpectrum.toPiLocalization_bijective.2 (Pi.single ⟨p, inferInstance⟩ 1)
  have : algebraMap R (Localization p.primeCompl) r = 1 := by
    simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩
  refine ⟨r, ?_, ?_, ?_⟩
  · rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
    simp
  · apply PrimeSpectrum.toPiLocalization_bijective.injective
    simp [map_mul, hr, ← Pi.single_mul]
  · intro q hq e
    have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
    have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
    rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
    simp

Premises used: Localization.AtPrime, IsLocalization.AtPrime.to_map_mem_maximal_iff, PrimeSpectrum.toPiLocalization_bijective, Function.Bijective.injective, map_mul, IsLocalization.AtPrime.isLocalRing, Pi.single_mul