awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
r r' : R
eq :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    ((toPiLocalization R : (a : R) → PiLocalization R) r' : PiLocalization R)
ne : ¬1 * r = 1 * r'
I : Ideal R
mI : I.IsMaximal
hI : Module.eqIdeal R r r' ≤ I
s : ↥I.primeCompl
hs : (↑s : R) * r = (↑s : R) * r'
⊢ False

Tactic:
exact s.2 (hI hs)

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
r : R
I : MaximalSpectrum R
⊢ Eq (α := Localization.AtPrime I.asIdeal)
    ((toPiLocalization R : (a : R) → PiLocalization R) r I : Localization.AtPrime I.asIdeal)
    ((algebraMap R (Localization.AtPrime I.asIdeal) : (a : R) → Localization.AtPrime I.asIdeal) r :
      Localization.AtPrime I.asIdeal)

Tactic:
rfl

Premises used: Quotient.mk', OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a :
  ∀ (r : R) (I : MaximalSpectrum S),
    Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
      ((((mapPiLocalization f hf).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
              RingHom.{u_1, u_2} R (PiLocalization S)) :
            (a : R) → PiLocalization S)
          r I :
        Localization.AtPrime I.asIdeal)
      ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
        Localization.AtPrime I.asIdeal)
⊢ (mapPiLocalization f hf).comp (↑(toPiLocalization R) : R →+* PiLocalization R) =
    RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f

Tactic:
ext r I
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
I : MaximalSpectrum S
a :
  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)
⊢ Eq.{u_2 + 1} (α := Localization.AtPrime I.asIdeal)
    ((((mapPiLocalization f hf).comp (↑(toPiLocalization R) : R →+* PiLocalization R) :
            RingHom.{u_1, u_2} R (PiLocalization S)) :
          (a : R) → PiLocalization S)
        r I :
      Localization.AtPrime I.asIdeal)
    ((RingHom.comp (AlgHom.toRingHom (toPiLocalization S)) f : (a : R) → PiLocalization S) r I :
      Localization.AtPrime I.asIdeal)

Tactic:
change Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)

Premises used: Algebra.algebraMap, Localization.localRingHom, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
I : MaximalSpectrum S
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 ⋯ : ↥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))
⊢ 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)

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]

Premises used: Localization.localRingHom_mk', Submonoid.coe_one, map_one, IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
r : R
I : MaximalSpectrum S
⊢ 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 ⋯ : ↥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:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R) ⋯) (RingHom.id (PiLocalization R))

Tactic:
RingHom.ext fun _ ↦ funext fun _ ↦ congr($(Localization.localRingHom_id _) _)

Premises used: MaximalSpectrum.asIdeal, Function.bijective_id, congrArg, Localization.AtPrime, MaximalSpectrum.mk, MaximalSpectrum.mapPiLocalization._proof_2, Localization.localRingHom_id, id, RingHom.ext, funext, Pi.evalRingHom, Ideal.comap, RingHom.id, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
f : R →+* S
g : S →+* P
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
hg : Function.Bijective.{u_2 + 1, u_3 + 1} (α := S) (β := P) (⇑g : (a : S) → P)
⊢ mapPiLocalization (g.comp f) ⋯ = (mapPiLocalization g hg).comp (mapPiLocalization f hf)

Tactic:
RingHom.ext fun _ ↦ funext fun _ ↦ congr($(Localization.localRingHom_comp _ _ _ _ rfl _ rfl) _)

Premises used: MaximalSpectrum.asIdeal, congrArg, Localization.AtPrime, MaximalSpectrum.mk, MaximalSpectrum.mapPiLocalization._proof_2, id, RingHom.ext, funext, RingHom.comp, Pi.evalRingHom, Ideal.comap, Localization.localRingHom_comp, Function.Bijective.comp, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_3 :
  Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)
refine_1 :
  (mapPiLocalization (↑f : R →+* S) hf).comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) = RingHom.id (PiLocalization S)
refine_2 :
  RingHom.comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) (mapPiLocalization (↑f : R →+* S) hf) =
    RingHom.id (PiLocalization R)
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)

Tactic:
let e := RingEquiv.ofRingHom (mapPiLocalization f hf)
    (mapPiLocalization (f.symm : S →+* R) f.symm.bijective) ?_ ?_
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
e : RingEquiv.{u_1, u_2} (PiLocalization R) (PiLocalization S) :=
  RingEquiv.ofRingHom (mapPiLocalization (↑f : R →+* S) hf) (mapPiLocalization (↑f.symm : S →+* R) ⋯) ⋯ ⋯
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)

Tactic:
e.bijective

Premises used: Set.Mem, setOf, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, RingEquiv.bijective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
e : RingEquiv.{u_1, u_2} (PiLocalization R) (PiLocalization S) :=
  RingEquiv.ofRingHom (mapPiLocalization (↑f : R →+* S) hf) (mapPiLocalization (↑f.symm : S →+* R) ⋯) ⋯ ⋯
⊢ Function.Bijective.{u_1 + 1, u_2 + 1} (α := PiLocalization R) (β := PiLocalization S)
    (⇑(mapPiLocalization f_1 hf) : (a : PiLocalization R) → PiLocalization S)

Tactic:
exact e.bijective

Premises used: RingEquiv.bijective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)) ⋯)
    (RingHom.id (PiLocalization S))
⊢ (mapPiLocalization (↑f : R →+* S) hf).comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) = RingHom.id (PiLocalization S)

Tactic:
rw [← mapPiLocalization_comp]

Premises used: MaximalSpectrum.mapPiLocalization_comp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_1 :
  Eq (α := PiLocalization S →+* PiLocalization S) (mapPiLocalization (RingHom.id S) ⋯) (RingHom.id (PiLocalization S))
⊢ Eq (α := PiLocalization S →+* PiLocalization S)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : R →+* S) (↑f.symm : S →+* R)) ⋯)
    (RingHom.id (PiLocalization S))

Tactic:
simp_rw [RingEquiv.comp_symm, mapPiLocalization_id]

Premises used: MaximalSpectrum.mapPiLocalization_id, RingEquiv.comp_symm
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_2 :
  Eq (α := PiLocalization R →+* PiLocalization R)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) ⋯)
    (RingHom.id (PiLocalization R))
⊢ RingHom.comp (mapPiLocalization (↑f.symm : S →+* R) ⋯) (mapPiLocalization (↑f : R →+* S) hf) =
    RingHom.id (PiLocalization R)

Tactic:
rw [← mapPiLocalization_comp]

Premises used: MaximalSpectrum.mapPiLocalization_comp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
f_1 : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f_1 : (a : R) → S)
f : R ≃+* S := RingEquiv.ofBijective f_1 hf
refine_2 :
  Eq (α := PiLocalization R →+* PiLocalization R) (mapPiLocalization (RingHom.id R) ⋯) (RingHom.id (PiLocalization R))
⊢ Eq (α := PiLocalization R →+* PiLocalization R)
    (mapPiLocalization (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) ⋯)
    (RingHom.id (PiLocalization R))

Tactic:
simp_rw [RingEquiv.symm_comp, mapPiLocalization_id]

Premises used: MaximalSpectrum.mapPiLocalization_id, RingEquiv.symm_comp
-- 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 :
  ∀ (J : Ideal ((i : ι) → R i)) (max : J.IsMaximal)
    (notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)), False
⊢ False

Tactic:
have ⟨J, max, notMem⟩ := PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite R
-- 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))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
obtain :
  ∀ (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

Tactic:
obtain ⟨r, hr⟩ := surj (Function.update 0 ⟨J, max⟩ 1)

Premises used: Function.update, MaximalSpectrum.mk, OfNat.ofNat
-- 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))
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
      (asIdeal
        { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }))
    ((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 := ⋯ } :
      Localization.AtPrime
        (asIdeal
          { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }))
    (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 := ⋯ }))

Tactic:
replace hr := congr_fun hr ⟨_, I.2.comap_piEvalRingHom⟩
-- 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))
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 := ⋯ }))
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 := ⋯ }) :
      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)
⊢ 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)

Tactic:
simp_rw [toPiLocalization_apply_apply,
      ← Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, hr]

Premises used: MaximalSpectrum.toPiLocalization_apply_apply, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply
-- 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))
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 := ⋯ }))
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))
⊢ 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))

Tactic:
simp_rw [Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero