awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 := ⋯ }))
⊢ Ne (α := MaximalSpectrum ((i : ι) → R i))
    { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
    { asIdeal := J, isMaximal := max }

Tactic:
fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩

Premises used: MaximalSpectrum.asIdeal, PrimeSpectrum.mk, PrimeSpectrum.ext, congrArg, MaximalSpectrum.isMaximal, id, Ideal.IsMaximal.isPrime, Exists.intro, Sigma.mk, Not
-- 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 := ⋯ }))
⊢ Ne (α := MaximalSpectrum ((i : ι) → R i))
    { asIdeal := Ideal.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
    { asIdeal := J, isMaximal := max }

Tactic:
exact fun h ↦ notMem ⟨⟨i, I.1, I.2.isPrime⟩, PrimeSpectrum.ext congr($h.1)⟩
-- 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)
⊢ 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)⟩
-- 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)
this : r = 0
⊢ 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⟩
-- 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
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 }))
⊢ 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

Premises used: map_zero, Function.update_self
-- 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
this : r = 0
hr :
  Eq (α := Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
    (0 { asIdeal := J, isMaximal := max }) 1
⊢ False

Tactic:
zero_ne_one hr

Premises used: zero_ne_one
-- 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
this : r = 0
hr :
  Eq (α := Localization.AtPrime (R := (i : ι) → R i) (asIdeal { asIdeal := J, isMaximal := max }))
    (0 { asIdeal := J, isMaximal := max }) 1
⊢ False

Tactic:
exact zero_ne_one hr

Premises used: zero_ne_one
-- 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)
h :
  Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
    (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
contrapose! :
  ∀ (h : Infinite ι),
    ¬Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
        (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))
⊢ Finite ι

Tactic:
contrapose! h
-- 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)
h : Infinite ι
⊢ ¬Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
      (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))

Tactic:
toPiLocalization_not_surjective_of_infinite _

Premises used: MaximalSpectrum.toPiLocalization_not_surjective_of_infinite
-- 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)
h : Infinite ι
⊢ ¬Function.Surjective (α := (i : ι) → R i) (β := PiLocalization ((i : ι) → R i))
      (⇑(toPiLocalization ((i : ι) → R i)) : (a : (i : ι) → R i) → PiLocalization ((i : ι) → R i))

Tactic:
exact toPiLocalization_not_surjective_of_infinite _

Premises used: MaximalSpectrum.toPiLocalization_not_surjective_of_infinite
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
⊢ 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))

Tactic:
replace surj := mapPiLocalization_bijective _ ⟨toPiLocalization_injective R, surj⟩
    |>.2.comp surj
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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))
⊢ 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

Premises used: AlgHom.coe_toRingHom, MaximalSpectrum.mapPiLocalization_naturality, RingHom.coe_comp
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
      (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))
⊢ Finite.{u_1 + 1} (MaximalSpectrum R)

Tactic:
finite_of_toPiLocalization_pi_surjective surj.of_comp

Premises used: Function.Surjective.of_comp, MaximalSpectrum.finite_of_toPiLocalization_pi_surjective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
      (⇑(AlgHom.toRingHom (toPiLocalization (PiLocalization R))) :
        (a : PiLocalization R) → PiLocalization (PiLocalization R))
      (⇑(AlgHom.toRingHom (toPiLocalization R)) : (a : R) → PiLocalization R))
⊢ Finite.{u_1 + 1} (MaximalSpectrum R)

Tactic:
exact finite_of_toPiLocalization_pi_surjective surj.of_comp

Premises used: Function.Surjective.of_comp, MaximalSpectrum.finite_of_toPiLocalization_pi_surjective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Function.Injective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)

Tactic:
fun _ _ eq ↦ MaximalSpectrum.toPiLocalization_injective R <|
    funext fun I ↦ congr_fun eq I.toPrimeSpectrum

Premises used: MaximalSpectrum.toPrimeSpectrum, funext, MaximalSpectrum.toPiLocalization_injective, Function.Injective, congr_fun
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Function.Surjective (α := PiLocalization R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(piLocalizationToMaximal R) : (a : PiLocalization R) → MaximalSpectrum.PiLocalization R)

Tactic:
fun r ↦ ⟨fun I ↦ if h : I.1.IsMaximal then r ⟨_, h⟩ else 0, funext fun _ ↦ dif_pos _⟩

Premises used: MaximalSpectrum.isMaximal, MaximalSpectrum.mk, dif_pos, dite, funext, Exists.intro, Ideal.IsMaximal, OfNat.ofNat, PrimeSpectrum.asIdeal, Function.Surjective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
h : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ Function.Bijective (α := PiLocalization R) (β := MaximalSpectrum.PiLocalization R)
    (⇑(piLocalizationToMaximal R) : (a : PiLocalization R) → MaximalSpectrum.PiLocalization R)

Tactic:
(piLocalizationToMaximalEquiv h).bijective

Premises used: PrimeSpectrum.piLocalizationToMaximalEquiv, RingEquiv.bijective
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R →ₐ[R] MaximalSpectrum.PiLocalization R) (AlgHom.comp (piLocalizationToMaximal R) (toPiLocalization R))
    (MaximalSpectrum.toPiLocalization R)

Tactic:
rfl

Premises used: Set.Mem, setOf, Pi.ringHom, MaximalSpectrum.toPiLocalization, Algebra.ofId, Quotient.mk', AlgHom.comp, OreLocalization.oreDiv, rfl
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
Goal:
R : Type u_1
inst : CommSemiring R
surj : Function.Surjective (α := R) (β := PiLocalization R) (⇑(toPiLocalization R) : (a : R) → PiLocalization R)
I : PrimeSpectrum R
have : ∀ (J : Ideal R) (max : J.IsMaximal) (le : I.asIdeal ≤ J), I.asIdeal.IsMaximal
⊢ I.asIdeal.IsMaximal

Tactic:
have ⟨J, max, le⟩ := I.1.exists_le_maximal I.2.ne_top
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
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 := ⋯ } 1 :
          (a : PrimeSpectrum R) → Localization (M := R) a.asIdeal.primeCompl)),
    I.asIdeal.IsMaximal
⊢ I.asIdeal.IsMaximal

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

Premises used: PrimeSpectrum.mk, Function.update, Ideal.IsMaximal.isPrime, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
by_contra : ∀ (h : ¬I.asIdeal.IsMaximal), False
⊢ I.asIdeal.IsMaximal

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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
⊢ 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)

Tactic:
have hJ : algebraMap _ _ r = _ := (congr_fun hr _).trans (Function.update_self ..)
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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)
⊢ 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)

Tactic:
have hI : algebraMap _ _ r = _ := congr_fun hr I
-- Module: Mathlib.RingTheory.Spectrum.Maximal.Localization
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 := ⋯ }
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)
⊢ False

Tactic:
rw [← IsLocalization.lift_eq (M := J.primeCompl) (S := Localization J.primeCompl), hJ, map_one,
    Function.update_of_ne] at hI

Premises used: IsLocalization.lift_eq, map_one, Function.update_of_ne