awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
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 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)
Tactic: have hJ : algebraMap _ _ r = _ := (congr_fun hr _).trans (Function.update_self ..)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
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 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)
Tactic: have hI : algebraMap _ _ r = _ := congr_fun hr I
-- 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
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 rw : ∀ (hI : Eq.{u_1 + 1} (α := Localization (M := R) I.asIdeal.primeCompl) 1 (0 I)), False
Tactic: rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI
-- 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
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)
rw : ∀ (hI : Eq.{u_1 + 1} (α := Localization (M := R) I.asIdeal.primeCompl) 1 (0 I)), False
⊢ False
have h₁ : ∀
  (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 := sorry }
          (1 : Localization (M := R) { asIdeal := J, isPrime := sorry : PrimeSpectrum R }.asIdeal.primeCompl) I :
        Localization (M := R) I.asIdeal.primeCompl)),
  I ≠ { asIdeal := J, isPrime := sorry }
Tactic: rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI
-- 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
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)
rw : ∀ (hI : Eq.{u_1 + 1} (α := Localization (M := R) I.asIdeal.primeCompl) 1 (0 I)), False
h₁ :
  ∀
    (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 := ⋯ }
⊢ False
have hg : ∀ (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)
Tactic: rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
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_1 :
  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)
eq : I = { asIdeal := J, isPrime := ⋯ }
⊢ False
have this : I.asIdeal = J
Tactic: have : I.1 = J := congr_arg (·.1) eq
-- 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
⊢ I.asIdeal.IsMaximal
have have : ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J), 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)⟩
-- 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
⊢ 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)),
  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)⟩
-- 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
⊢ 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), 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)⟩
-- 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
⊢ 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)),
  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)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
⊢ (mapPiLocalization f).comp (↑(toPiLocalization R) : R →+* PiLocalization R) =
    RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f
have a : ∀ (r : R) (I : PrimeSpectrum S),
  Eq.{u_2 + 1} (α := Localization (M := S) I.asIdeal.primeCompl)
    ((((mapPiLocalization f).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
            RingHom.{u_1, u_2} R (PiLocalization S)) :
          (a : R) → PiLocalization S)
        r I :
      Localization (M := S) I.asIdeal.primeCompl)
    ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
      Localization (M := S) I.asIdeal.primeCompl)
Tactic: ext r I
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ Eq.{u_2 + 1} (α := Localization (M := S) I.asIdeal.primeCompl)
    ((((mapPiLocalization f).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
            RingHom.{u_1, u_2} R (PiLocalization S)) :
          (a : R) → PiLocalization S)
        r I :
      Localization (M := S) I.asIdeal.primeCompl)
    ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
      Localization (M := S) I.asIdeal.primeCompl)
have a : Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
  (((Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f sorry :
          RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f I.asIdeal)) (Localization.AtPrime I.asIdeal)) :
        (a : Localization.AtPrime (Ideal.comap f I.asIdeal)) → Localization.AtPrime I.asIdeal)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal)) :
          (a : R) → Localization.AtPrime (Ideal.comap f I.asIdeal))
        r) :
    Localization.AtPrime I.asIdeal)
  ((algebraMap S (Localization.AtPrime I.asIdeal) : (a : S) → Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r) :
    Localization.AtPrime I.asIdeal)
Tactic: change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
r : R
I : PrimeSpectrum S
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    (((Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f I.asIdeal)) (Localization.AtPrime I.asIdeal)) :
          (a : Localization.AtPrime (Ideal.comap f I.asIdeal)) → Localization.AtPrime I.asIdeal)
        ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal)) :
            (a : R) → Localization.AtPrime (Ideal.comap f I.asIdeal))
          r) :
      Localization.AtPrime I.asIdeal)
    ((algebraMap S (Localization.AtPrime I.asIdeal) : (a : S) → Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r) :
      Localization.AtPrime I.asIdeal)
have a : Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
  (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
    (Subtype.mk (p := fun (x : S) ↦ x ∈ I.asIdeal.primeCompl) 1 sorry : ↥I.asIdeal.primeCompl))
  (IsLocalization.mk' (R := S) (M := I.asIdeal.primeCompl) (Localization.AtPrime I.asIdeal) ((f : (a : R) → S) r : S)
    (1 : ↥I.asIdeal.primeCompl))
Tactic: simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
    ← IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R)) (RingHom.id (PiLocalization R))
have a : ∀ (x : PiLocalization R) (x_1 : PrimeSpectrum R),
  Eq (α := Localization (M := R) x_1.asIdeal.primeCompl)
    ((mapPiLocalization (RingHom.id R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
      Localization (M := R) x_1.asIdeal.primeCompl)
    ((RingHom.id (PiLocalization R) : (a : PiLocalization R) → PiLocalization R) x x_1 :
      Localization (M := R) x_1.asIdeal.primeCompl)
Tactic: ext