-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
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))
    (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 := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl)),
    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))
    (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 := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl))
    (hI : Eq.{u_1 + 1} (α := Localization (M := R) I.asIdeal.primeCompl) 1 (0 I)), False
h :
  ∀ (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))
    (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 := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl))
    (hI :
      Eq (α := Localization (M := R) I.asIdeal.primeCompl) (1 : Localization (M := R) I.asIdeal.primeCompl)
        (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
            { asIdeal := J, isPrime := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl)),
    I ≠ { asIdeal := J, isPrime := ⋯ }
hg :
  ∀ (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))
    (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 := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl))
    (y : ↥J.primeCompl),
    IsUnit (M := Localization (M := R) I.asIdeal.primeCompl)
      ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl)
          (↑y : R) :
        Localization (M := R) I.asIdeal.primeCompl)
h₁ :
  ∀ (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))
    (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 := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl))
    (hI :
      Eq (α := Localization (M := R) I.asIdeal.primeCompl) (1 : Localization (M := R) I.asIdeal.primeCompl)
        (Function.update (β := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl) 0
            { asIdeal := J, isPrime := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl)),
    I ≠ { asIdeal := J, isPrime := ⋯ }
hg₁ hg₂ :
  ∀ (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))
    (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 := ⋯ }
            (1 : Localization (M := R) { asIdeal := J, isPrime := ⋯ : PrimeSpectrum R }.asIdeal.primeCompl) I :
          Localization (M := R) I.asIdeal.primeCompl))
    (y : ↥J.primeCompl),
    IsUnit (M := Localization (M := R) I.asIdeal.primeCompl)
      ((algebraMap R (Localization (M := R) I.asIdeal.primeCompl) : (a : R) → Localization I.asIdeal.primeCompl)
          (↑y : R) :
        Localization (M := R) I.asIdeal.primeCompl)
⊢ I.asIdeal.IsMaximal

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

Premises used: map_one, Function.update_of_ne