-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
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))
    (this : r = 0), False
have₅ :
  ∀ (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₆ :
  ∀ (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 }))
        (0 { asIdeal := J, isMaximal := max }) 1),
    False
⊢ 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

Premises used: map_zero, Function.update_self