-- 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)
        (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 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)
have 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 { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := sorry }))
  ((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: rw [Function.update_of_ne]