-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
have have₁ have₂ : ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J), I.asIdeal.IsMaximal
have₃ :
  ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J) (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
            { asIdeal := J, isPrime := ⋯ } 1 :
          (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)),
    I.asIdeal.IsMaximal
have₄ :
  ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J) (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
            { asIdeal := J, isPrime := ⋯ } 1 :
          (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl))
    (h : ¬I.asIdeal.IsMaximal), False
have₅ :
  ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J) (r : R)
    (hr :
      Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
        (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
            { asIdeal := J, isPrime := ⋯ } 1 :
          (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl))
    (h : ¬I.asIdeal.IsMaximal)
    (hJ :
      Eq (α := Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
        ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) :
              (a : R) → Localization { asIdeal := J, isPrime := ⋯ }.asIdeal.primeCompl)
            r :
          Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)
        (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl)),
    False
⊢ I.asIdeal.IsMaximal
have have₆ : ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J) (r : R)
  (hr :
    Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
      (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
          { asIdeal := J, isPrime := sorry } 1 :
        (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl))
  (h : ¬I.asIdeal.IsMaximal)
  (hJ :
    Eq (α := Localization (M := R) { asIdeal := J, isPrime := sorry : PrimeSpectrum R }.asIdeal.primeCompl)
      ((algebraMap R (Localization (M := R) { asIdeal := J, isPrime := sorry : PrimeSpectrum R }.asIdeal.primeCompl) :
            (a : R) → Localization { asIdeal := J, isPrime := sorry }.asIdeal.primeCompl)
          r :
        Localization (M := R) { asIdeal := J, isPrime := sorry : PrimeSpectrum R }.asIdeal.primeCompl)
      (1 : Localization (M := R) { asIdeal := J, isPrime := sorry : PrimeSpectrum R }.asIdeal.primeCompl))
  (hI :
    Eq (α := Localization (M := R) I.asIdeal.primeCompl)
      ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl) r :
        Localization (M := R) I.asIdeal.primeCompl)
      (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
          { asIdeal := J, isPrime := sorry }
          (1 : Localization (M := R) { asIdeal := J, isPrime := sorry : PrimeSpectrum R }.asIdeal.primeCompl) I :
        Localization (M := R) I.asIdeal.primeCompl)),
  False
Tactic: classical
  have ⟨J, max, le⟩ := I.1.exists_le_maximal I.2.ne_top
  obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max.isPrime⟩ 1)
  by_contra h
  have hJ : algebraMap _ _ r = _ := (congr_fun hr _).trans (Function.update_self ..)
  have hI : algebraMap _ _ r = _ := congr_fun hr I
  rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI
  · exact one_ne_zero hI
  · intro eq; have : I.1 = J := congr_arg (·.1) eq; exact h (this ▸ max)
  · exact fun ⟨s, hs⟩ ↦ IsLocalization.map_units (M := I.1.primeCompl) _ ⟨s, fun h ↦ hs (le h)⟩