awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr :
  Eq (α := PiLocalization ((i : ι) → R i))
    ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
      PiLocalization ((i : ι) → R i))
    (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max } 1 :
      (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal)
i : ι
I : MaximalSpectrum (R i)
⊢ Eq (α := Localization.AtPrime I.asIdeal)
    ((toPiLocalization (R i) : (a : R i) → PiLocalization (R i)) (r i) I : Localization.AtPrime I.asIdeal)
    ((toPiLocalization (R i) : (a : R i) → PiLocalization (R i)) (0 i) I : Localization.AtPrime I.asIdeal)
have hr₁ : Eq (α :=
  Localization.AtPrime
    (asIdeal { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry }))
  ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r
      { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry } :
    Localization.AtPrime
      (asIdeal
        { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry }))
  (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
      { asIdeal := J, isMaximal := max }
      (1 : Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
      { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry } :
    Localization.AtPrime
      (asIdeal
        { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry }))
Tactic: replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  Eq (α := Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal))
    ((algebraMap ((i : ι) → R i)
            (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal)) :
          (a : (i : ι) → R i) → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))
        r :
      Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal))
    (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max }
        (1 : Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
        { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ } :
      Localization.AtPrime
        (asIdeal
          { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }))
⊢ Eq (α := Localization.AtPrime I.asIdeal)
    ((toPiLocalization (R i) : (a : R i) → PiLocalization (R i)) (r i) I : Localization.AtPrime I.asIdeal)
    ((toPiLocalization (R i) : (a : R i) → PiLocalization (R i)) (0 i) I : Localization.AtPrime I.asIdeal)
have simp_rw : Eq.{u_4 + 1} (α := Localization.AtPrime I.asIdeal)
  ((Localization.AtPrime.mapPiEvalRingHom (R := R) I.asIdeal :
        (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal)) → Localization.AtPrime I.asIdeal)
      (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max }
        (1 : Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
        { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry }) :
    Localization.AtPrime I.asIdeal)
  ((Localization.AtPrime.mapPiEvalRingHom (R := R) I.asIdeal :
        (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal)) → Localization.AtPrime I.asIdeal)
      ((algebraMap ((i : ι) → R i)
            (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal)) :
          (a : (i : ι) → R i) → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))
        0) :
    Localization.AtPrime I.asIdeal)
Tactic: simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  Eq (α := Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal))
    ((algebraMap ((i : ι) → R i)
            (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal)) :
          (a : (i : ι) → R i) → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))
        r :
      Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal))
    (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max }
        (1 : Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
        { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ } :
      Localization.AtPrime
        (asIdeal
          { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }))
⊢ Eq.{u_4 + 1} (α := Localization.AtPrime I.asIdeal)
    ((Localization.AtPrime.mapPiEvalRingHom (R := R) I.asIdeal :
        (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal)) → Localization.AtPrime I.asIdeal)
      (0 { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }))
    ((Localization.AtPrime.mapPiEvalRingHom (R := R) I.asIdeal :
        (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal)) → Localization.AtPrime I.asIdeal)
      ((algebraMap ((i : ι) → R i)
            (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal)) :
          (a : (i : ι) → R i) → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))
        0))
have simp_rw : Eq.{u_4 + 1} (α := Localization.AtPrime I.asIdeal)
  ((Localization.AtPrime.mapPiEvalRingHom (R := R) I.asIdeal :
      (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal)) → Localization.AtPrime I.asIdeal)
    0)
  ((Localization.AtPrime.mapPiEvalRingHom (R := R) I.asIdeal :
      (a : Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal)) → Localization.AtPrime I.asIdeal)
    ((algebraMap ((i : ι) → R i)
          (Localization.AtPrime (Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal)) :
        (a : (i : ι) → R i) → Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))
      0))
Tactic: simp_rw [Pi.zero_apply, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr :
  Eq (α := PiLocalization ((i : ι) → R i))
    ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
      PiLocalization ((i : ι) → R i))
    (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max } 1 :
      (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal)
⊢ False
have this : r = 0
Tactic: have : r = 0 := funext fun i ↦ toPiLocalization_injective _ <| funext fun I ↦ by
    replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
    dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr
    simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
    rw [Function.update_of_ne]; · simp_rw [Pi.zero_apply, map_zero]
    exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
hr :
  Eq (α := PiLocalization ((i : ι) → R i))
    ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
      PiLocalization ((i : ι) → R i))
    (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max } 1 :
      (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal)
this : r = 0
⊢ False
have hr₁ : Eq (α := Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
  ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r
      { asIdeal := J, isMaximal := max } :
    Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
  (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
      { asIdeal := J, isMaximal := max }
      (1 : Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
      { asIdeal := J, isMaximal := max } :
    Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
Tactic: replace hr := congr_fun hr ⟨J, max⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
this : r = 0
hr :
  Eq (α := Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
    ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r
        { asIdeal := J, isMaximal := max } :
      Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
    (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
        { asIdeal := J, isMaximal := max }
        (1 : Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
        { asIdeal := J, isMaximal := max } :
      Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
⊢ False
have hr₁ : Eq (α := Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
  (0 { asIdeal := J, isMaximal := max }) 1
Tactic: rw [this, map_zero, Function.update_self] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ False
have have : ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
  (notMem : { asIdeal := J, isPrime := sorry } ∉ Set.range (PrimeSpectrum.sigmaToPi R)), False
Tactic: classical
  have ⟨J, max, notMem⟩ := PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite R
  obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max⟩ 1)
  have : r = 0 := funext fun i ↦ toPiLocalization_injective _ <| funext fun I ↦ by
    replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
    dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr
    simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
    rw [Function.update_of_ne]; · simp_rw [Pi.zero_apply, map_zero]
    exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩
  replace hr := congr_fun hr ⟨J, max⟩
  rw [this, map_zero, Function.update_self] at hr
  exact zero_ne_one hr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
have have₁ have₂ :
  ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
    (notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)), False
⊢ False
have have₃ : ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
  (notMem : { asIdeal := J, isPrime := sorry } ∉ Set.range (PrimeSpectrum.sigmaToPi R)) (r : (i : ι) → R i)
  (hr :
    Eq (α := PiLocalization ((i : ι) → R i))
      ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
        PiLocalization ((i : ι) → R i))
      (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
          { asIdeal := J, isMaximal := max } 1 :
        (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal)),
  False
Tactic: classical
  have ⟨J, max, notMem⟩ := PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite R
  obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max⟩ 1)
  have : r = 0 := funext fun i ↦ toPiLocalization_injective _ <| funext fun I ↦ by
    replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
    dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr
    simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
    rw [Function.update_of_ne]; · simp_rw [Pi.zero_apply, map_zero]
    exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩
  replace hr := congr_fun hr ⟨J, max⟩
  rw [this, map_zero, Function.update_self] at hr
  exact zero_ne_one hr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
inst_2 : Infinite ι
surj :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
have have₁ have₂ :
  ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
    (notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)), False
have₃ :
  ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
    (notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)) (r : (i : ι) → R i)
    (hr :
      Eq (α := PiLocalization ((i : ι) → R i))
        ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
          PiLocalization ((i : ι) → R i))
        (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
            { asIdeal := J, isMaximal := max } 1 :
          (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal)),
    False
⊢ False
have have₄ : ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
  (notMem : { asIdeal := J, isPrime := sorry } ∉ Set.range (PrimeSpectrum.sigmaToPi R)) (r : (i : ι) → R i)
  (hr :
    Eq (α := PiLocalization ((i : ι) → R i))
      ((toPiLocalization ((i : ι) → R i) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i)) r :
        PiLocalization ((i : ι) → R i))
      (Function.update (β := fun (I : MaximalSpectrum ((i : ι) → R i)) ↦ Localization.AtPrime I.asIdeal) 0
          { asIdeal := J, isMaximal := max } 1 :
        (a : MaximalSpectrum ((i : ι) → R i)) → Localization.AtPrime a.asIdeal))
  (this : r = 0), False
Tactic: classical
  have ⟨J, max, notMem⟩ := PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite R
  obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max⟩ 1)
  have : r = 0 := funext fun i ↦ toPiLocalization_injective _ <| funext fun I ↦ by
    replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
    dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr
    simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]
    rw [Function.update_of_ne]; · simp_rw [Pi.zero_apply, map_zero]
    exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩
  replace hr := congr_fun hr ⟨J, max⟩
  rw [this, map_zero, Function.update_self] at hr
  exact zero_ne_one hr
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (goal)
Goal:
ι : Type u_5
R : ι → Type u_4
inst : (i : ι) → CommSemiring (R i)
inst_1 : ∀ (i : ι), Nontrivial.{u_4} (R i)
h :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ Finite ι
have contrapose! : ∀ (h : Infinite ι),
  ¬Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
      (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
Tactic: contrapose! h
Cleared hypotheses: h
-- 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)
⊢ Finite.{u_1 + 1} (MaximalSpectrum R)
have surj₁ : Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
  (Function.comp (β := PiLocalization R)
    (⇑(mapPiLocalization (AlgHom.toRingHom (toPiLocalization R)) sorry) :
      (a : PiLocalization R) → PiLocalization (PiLocalization R))
    (⇑(toPiLocalization R) : (a : R) → PiLocalization R))
Tactic: replace surj := mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩
    |>.2.comp surj
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Maximal.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
surj_1 : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
surj :
  Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
    (Function.comp (β := PiLocalization R)
      (⇑(mapPiLocalization (AlgHom.toRingHom (toPiLocalization R)) ⋯) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(toPiLocalization R) : (a : R) → PiLocalization R))
⊢ Finite.{u_1 + 1} (MaximalSpectrum R)
have surj₁ : Function.Surjective (α := R) (β := PiLocalization (PiLocalization R))
  (Function.comp (β := PiLocalization R)
    (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
      (a : PiLocalization R) → PiLocalization (PiLocalization R))
    (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))
Tactic: rw [← AlgHom.coe_toRingHom,
    ← RingHom.coe_comp, mapPiLocalization_naturality, RingHom.coe_comp] at surj
Cleared hypotheses: surj
-- 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: have ⟨J, max, le⟩ := I.1.exists_le_maximal I.2.ne_top
-- 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
⊢ I.asIdeal.IsMaximal
have obtain : ∀ (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: obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max.isPrime⟩ 1)
-- 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)
⊢ I.asIdeal.IsMaximal
have by_contra : ∀ (h : ¬I.asIdeal.IsMaximal), False
Tactic: by_contra h