awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
p : LTSeries (PrimeSpectrum R)
hx :
  x ∈
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p).asIdeal
hp :
  p.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    0
h :
  p.toFun (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2})
      (Fin.last
        (p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}))) =
    RelSeries.last (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}) p
⊢ p.toFun (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}) 0 =
    RelSeries.last (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}) p
have h₁ : p.toFun (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2})
    (Fin.last
      (p.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}))) =
  p.toFun (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2})
    (Fin.last (p.length (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2})))
Tactic: rw [show 0 = Fin.last p.length from Fin.zero_eq_mk.mpr hp, RelSeries.last]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R))
    (hx :
      x ∈
        (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            p).asIdeal)
    (hp :
      p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}) =
        n),
    ∃ (q : LTSeries (PrimeSpectrum R)),
      x ∈
          (q.toFun (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              1).asIdeal ∧
        n =
            q.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}) ∧
          RelSeries.head (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                p =
              RelSeries.head (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q ∧
            RelSeries.last (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                p =
              RelSeries.last (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q
p : LTSeries (PrimeSpectrum R)
hx :
  x ∈
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        p).asIdeal
hp :
  p.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b}) =
    n + 1
h0 : n = 0
⊢ Eq (α :=
    Fin
      (p.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}) +
        1))
    1
    (Fin.last
      (p.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})))
have rw : Eq (α := Fin (HAdd.hAdd (α := ℕ) 1 1)) 1 ⟨1, sorry⟩
Tactic: rw [Fin.last, hp, h0, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
inst_4 : Nontrivial M
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) (closedPoint R)
have obtain : ∀ (p : PrimeSpectrum R) (hp : Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) p),
  Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M) (closedPoint R)
Tactic: obtain ⟨p, hp⟩ := (Module.nonempty_support_iff (R := R)).mpr ‹_›
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
⊢ Subsingleton (LocalizedModule.Away f M) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
have rw : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
  Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
Tactic: rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    disjoint_compl_left_iff, Set.le_iff_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
⊢ Subsingleton (LocalizedModule.Away f M) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
have rw₁ : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
  Disjoint (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.support R M)
Tactic: rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    disjoint_compl_left_iff, Set.le_iff_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
    Disjoint (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.support R M)
⊢ Subsingleton (LocalizedModule.Away f M) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
have rw₂ : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
  LE.le (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
Tactic: rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    disjoint_compl_left_iff, Set.le_iff_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : R
rw :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
rw₁ :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
    Disjoint (α := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus {f})ᶜ (Module.support R M)
rw₂ :
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
    LE.le (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
⊢ Subsingleton (LocalizedModule.Away f M) ↔
    Disjoint (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum R)) (Module.support R M)
have rw₃ : Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f}) ↔
  Subset (α := Set (PrimeSpectrum R)) (Module.support R M) (PrimeSpectrum.zeroLocus {f})
Tactic: rw [subsingleton_iff_support_subset, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
    disjoint_compl_left_iff, Set.le_iff_subset]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
⊢ IsClosed (X := PrimeSpectrum R) (support R M)
have rw : IsClosed (X := PrimeSpectrum R) (PrimeSpectrum.zeroLocus (↑(annihilator R M) : Set R))
Tactic: rw [support_eq_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
x : PrimeSpectrum A
hx : Membership.mem (γ := Set (PrimeSpectrum A)) (support A M) x
⊢ Membership.mem (γ := Set (PrimeSpectrum A))
    (Set.preimage (β := PrimeSpectrum R) (PrimeSpectrum.comap (algebraMap R A)) (support R M)) x
have simp : ∀ (hx : ∃ (m : M), ∀ (r : A), r • m = 0 → r ∈ x.asIdeal),
  ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)
Tactic: simp only [Set.mem_preimage, mem_support_iff', PrimeSpectrum.comap_asIdeal, Ideal.mem_comap,
    ne_eq, not_imp_not] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Module (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
x : PrimeSpectrum A
hx : ∃ (m : M), ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
⊢ ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)
have obtain : ∀ (m : M) (hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal),
  ∃ (m : M), ∀ (r : R), r • m = 0 → Membership.mem (α := A) x.asIdeal ((algebraMap R A : (a : R) → A) r : A)
Tactic: obtain ⟨m, hm⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
⊢ Set.Finite.{u} (α := PrimeSpectrum R) {x : PrimeSpectrum R | IsMin x}
have this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
Tactic: have : Function.Injective (asIdeal (R := R)) := @PrimeSpectrum.ext _ _
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
⊢ Set.Finite.{u} (α := PrimeSpectrum R) {x : PrimeSpectrum R | IsMin x}
have refine : Set.Finite.{u} (α := Ideal R) (asIdeal '' {x : PrimeSpectrum R | IsMin x})
Tactic: refine Set.Finite.of_finite_image (f := asIdeal) ?_ this.injOn
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : IsNoetherianRing R
this : Function.Injective.{u + 1, u + 1} (α := PrimeSpectrum R) asIdeal
⊢ Set.Finite.{u} (α := Ideal R) (asIdeal '' {x : PrimeSpectrum R | IsMin x})
have simp_rw : Set.Finite.{u} (α := Ideal R)
  (asIdeal '' {x : PrimeSpectrum R | Membership.mem (γ := Set (Ideal R)) (minimalPrimes R) x.asIdeal})
Tactic: simp_rw [isMin_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have obtain : ∀ (r : R)
  (hr :
    Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
      (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
          { asIdeal := p, isPrime := sorry } 1 :
        (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)),
  ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Tactic: obtain ⟨r, hr⟩ := PrimeSpectrum.toPiLocalization_bijective.2 (Pi.single ⟨p, inferInstance⟩ 1)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have this : Eq (α := Localization (M := R) p.primeCompl)
  ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
    Localization (M := R) p.primeCompl)
  (1 : Localization (M := R) p.primeCompl)
Tactic: have : algebraMap R (Localization p.primeCompl) r = 1 := by
    simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have refine_1 : r ∉ p
Tactic: refine ⟨r, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
refine_1 : r ∉ p
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have refine_2 : IsIdempotentElem r
Tactic: refine ⟨r, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
refine_1 : r ∉ p
refine_2 : IsIdempotentElem r
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have refine_3 : ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Tactic: refine ⟨r, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
⊢ r ∉ p
have refine_1 : 1 ∉ IsLocalRing.maximalIdeal (Localization.AtPrime p)
Tactic: rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
⊢ IsIdempotentElem r
have refine_2 : Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) (r * r) : PiLocalization R)
  ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
Tactic: apply PrimeSpectrum.toPiLocalization_bijective.injective
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
⊢ r ∈ q
have this₁ : { asIdeal := q, isPrime := sorry : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := sorry }
Tactic: have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this_1 :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this : { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }
⊢ r ∈ q
have this₁ : Eq (α := Localization.AtPrime q)
  ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r : Localization.AtPrime q)
  (0 : Localization.AtPrime q)
Tactic: have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
r : R
hr :
  Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
    (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
        { asIdeal := p, isPrime := ⋯ } 1 :
      (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)
this_1 :
  Eq (α := Localization (M := R) p.primeCompl)
    ((algebraMap R (Localization (M := R) p.primeCompl) : (a : R) → Localization p.primeCompl) r :
      Localization (M := R) p.primeCompl)
    (1 : Localization (M := R) p.primeCompl)
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this_2 : { asIdeal := q, isPrime := ⋯ : PrimeSpectrum R } ≠ { asIdeal := p, isPrime := ⋯ }
this :
  Eq (α := Localization.AtPrime q)
    ((algebraMap R (Localization.AtPrime q) : (a : R) → Localization.AtPrime q) r : Localization.AtPrime q)
    (0 : Localization.AtPrime q)
⊢ r ∈ q
have refine_3 : Membership.mem (γ := Ideal (Localization.AtPrime q)) (IsLocalRing.maximalIdeal (Localization.AtPrime q)) 0
Tactic: rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Noetherian (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsArtinianRing R
p : Ideal R
inst_2 : p.IsPrime
⊢ ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
have obtain : ∀ (r : R)
  (hr :
    Eq (α := PiLocalization R) ((toPiLocalization R : (a : R) → PiLocalization R) r : PiLocalization R)
      (Pi.single (M := fun (p : PrimeSpectrum R) ↦ Localization (M := R) p.asIdeal.primeCompl)
          { asIdeal := p, isPrime := sorry } 1 :
        (j : PrimeSpectrum R) → Localization (M := R) j.asIdeal.primeCompl)),
  ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q
Tactic: classical
  obtain ⟨r, hr⟩ := PrimeSpectrum.toPiLocalization_bijective.2 (Pi.single ⟨p, inferInstance⟩ 1)
  have : algebraMap R (Localization p.primeCompl) r = 1 := by
    simpa [PrimeSpectrum.toPiLocalization,
      -FaithfulSMul.algebraMap_eq_one_iff] using funext_iff.mp hr ⟨p, inferInstance⟩
  refine ⟨r, ?_, ?_, ?_⟩
  · rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime p) p, this]
    simp
  · apply PrimeSpectrum.toPiLocalization_bijective.injective
    simp [map_mul, hr, ← Pi.single_mul]
  · intro q hq e
    have : PrimeSpectrum.mk q inferInstance ≠ ⟨p, inferInstance⟩ := ne_of_apply_ne (·.1) e
    have : (algebraMap R (Localization.AtPrime q)) r = 0 := by
      simpa [PrimeSpectrum.toPiLocalization, this,
        -FaithfulSMul.algebraMap_eq_zero_iff] using funext_iff.mp hr ⟨q, inferInstance⟩
    rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q, this]
    simp