awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Jacobson (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsJacobsonRing R
x : PrimeSpectrum R
tfae_1_to_2 : ∀ (a : IsOpen (X := PrimeSpectrum R) {x}), IsClopen (X := PrimeSpectrum R) {x}
tfae_2_to_3 :
  ∀ (a : IsClopen (X := PrimeSpectrum R) {x}),
    IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}
⊢ [IsOpen (X := PrimeSpectrum R) {x}, IsClopen (X := PrimeSpectrum R) {x},
      IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}].TFAE
have tfae_3_to_1 : ∀ (a : IsClosed (X := PrimeSpectrum R) {x} ∧ StableUnderGeneralization (X := PrimeSpectrum R) {x}),
  IsOpen (X := PrimeSpectrum R) {x}
Tactic: tfae_have 3 → 1
  | ⟨h₁, h₂⟩ => by
    rw [isClosed_singleton_iff_isMaximal, ← isMax_iff] at h₁
    suffices {x} = (⋃ p ∈ { p : PrimeSpectrum R | IsMin p ∧ p ≠ x }, closure {p})ᶜ by
      rw [this, isOpen_compl_iff]
      refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
      exact (finite_setOf_isMin R).subset fun x h ↦ h.1
    ext p
    simp only [Set.mem_singleton_iff, ne_eq, Set.mem_setOf_eq, Set.compl_iUnion, Set.mem_iInter,
      Set.mem_compl_iff, and_imp, ← specializes_iff_mem_closure, ← le_iff_specializes,
      not_imp_not]
    constructor
    · rintro rfl _ _
      rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂
      exact h₂.eq_of_le
    · intro hp
      apply h₁.eq_of_ge
      obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
      exact (hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
have pos : ∀ (hn : x ∈ p₀.asIdeal), ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
Tactic: by_cases hn : x ∈ p₀.1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
pos : ∀ (hn : x ∈ p₀.asIdeal), ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
have neg : ∀ (hn : x ∉ p₀.asIdeal), ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
Tactic: by_cases hn : x ∈ p₀.1
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
have neg : ∀ (q : Ideal R) (hq : q ∈ (p₀.asIdeal + span {x}).minimalPrimes),
  ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
Tactic: obtain ⟨q, hq⟩ := (p₀.1 + span {x}).nonempty_minimalPrimes <|
    sup_le (IsLocalRing.le_maximalIdeal_of_isPrime p₀.1) ((span_singleton_le_iff_mem 𝔪).mpr hx)
      |>.trans_lt (IsMaximal.isPrime' 𝔪).1.lt_top |>.ne
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
have this : q.asIdeal.IsPrime
Tactic: have : q.1.IsPrime := q.2
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
have hxq : x ∈ q.asIdeal
Tactic: have hxq : x ∈ q.1 := le_sup_right.trans hq.1.2 (mem_span_singleton_self x)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
have neg : q.asIdeal < 𝔪
Tactic: refine ⟨q, hxq, lt_of_le_not_ge (le_sup_left.trans hq.1.2) fun h ↦ hn (h hxq), ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
⊢ q.asIdeal < 𝔪
have neg : ∀ (hqm : q.asIdeal = 𝔪), False
Tactic: refine lt_of_le_of_ne (IsLocalRing.le_maximalIdeal_of_isPrime q.1) fun hqm ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
⊢ False
have h : height.{u_1} (R := R ⧸ p₀.asIdeal)
    (asIdeal
      ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) q sorry))) ≤
  1
Tactic: have h : (e ⟨q, le_sup_left.trans hq.1.2⟩).1.height ≤ 1 :=
    map_height_le_one_of_mem_minimalPrimes hq
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h :
  height.{u_1} (R := R ⧸ p₀.asIdeal)
      (asIdeal
        ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) q ⋯))) ≤
    1
⊢ False
have h₂ : height.{u_1} (R := R ⧸ p₀.asIdeal)
    (asIdeal
      ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) (closedPoint R) sorry))) ≤
  1
Tactic: simp_rw [show q = closedPoint R from PrimeSpectrum.ext hqm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h :
  height.{u_1} (R := R ⧸ p₀.asIdeal)
      (asIdeal
        ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) (closedPoint R) ⋯))) ≤
    1
⊢ False
have hph : height.{u_1} (R := R ⧸ p₀.asIdeal)
    (asIdeal
      ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) p₁ sorry))) ≤
  0
Tactic: have hph : (e ⟨p₁, h₀.le⟩).1.height ≤ 0 :=
    Order.lt_one_iff_nonpos.mp (height_le_iff.mp h _ inferInstance (by simpa using h₁))
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : Membership.mem (γ := Ideal R) 𝔪 x
hn : x ∉ p₀.asIdeal
e : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) :=
  p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q_1 : Ideal R
hq : q_1 ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q_1, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h :
  height.{u_1} (R := R ⧸ p₀.asIdeal)
      (asIdeal
        ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) (closedPoint R) ⋯))) ≤
    1
hph :
  height.{u_1} (R := R ⧸ p₀.asIdeal)
      (asIdeal
        ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
          (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
            Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) p₁ ⋯))) ≤
    0
⊢ False
have neg : LT.lt.{u_1} (α := Ideal (R ⧸ p₀.asIdeal))
  (asIdeal
    ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) p₀ sorry)))
  (asIdeal
    ((e : (a : (↑(zeroLocus (↑p₀.asIdeal : Set R)) : Type u_1)) → PrimeSpectrum (R ⧸ p₀.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑p₀.asIdeal : Set R)) x) p₁ sorry)))
Tactic: refine not_lt_zero (a := (e ⟨p₀, le_refl p₀⟩).1.height) (height_le_iff.mp hph _ inferInstance ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o
  (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
have hm : Eq.{u_1 + 1} (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) (closedPoint (Localization.AtPrime p₂.asIdeal))
  ((e.symm :
      (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1)) →
        PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry : PrimeSpectrum R })
      p₂ sorry))
Tactic: have hm : closedPoint (Localization.AtPrime p₂.1) =
    e.symm ⟨p₂, le_refl p₂⟩ := (PrimeSpectrum.ext Localization.AtPrime.map_eq_maximalIdeal).symm
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o
  (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm :
  Eq.{u_1 + 1} (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) (closedPoint (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₂ ⋯))
⊢ Membership.mem (α := Localization.AtPrime p₂.asIdeal) (γ := Ideal (Localization.AtPrime p₂.asIdeal))
    (maximalIdeal (Localization.AtPrime p₂.asIdeal))
    ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
      Localization.AtPrime p₂.asIdeal)
have rw : Membership.mem (α := Localization.AtPrime p₂.asIdeal) (γ := Ideal (Localization.AtPrime p₂.asIdeal))
  (map (F := R →+* Localization.AtPrime p₂.asIdeal) (algebraMap R (Localization.AtPrime p₂.asIdeal)) p₂.asIdeal)
  ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
    Localization.AtPrime p₂.asIdeal)
Tactic: rw [← Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o
  (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm :
  Eq.{u_1 + 1} (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) (closedPoint (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₂ ⋯))
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
have obtain : ∀ (q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
  (hxq :
    Membership.mem (α := Localization.AtPrime p₂.asIdeal) q.asIdeal
      ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
        Localization.AtPrime p₂.asIdeal))
  (h₀ :
    (e.symm :
          (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1)) →
            PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
        (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
          x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry : PrimeSpectrum R }) p₀ sorry) <
      q)
  (h₁ : q.asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)),
  ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
Tactic: obtain ⟨q, hxq, h₀, h₁⟩ :=
    @exist_mem_one_of_mem_maximal_ideal (Localization.AtPrime p₂.1) _ _ _
      (e.symm ⟨p₁, h₁.le⟩) (e.symm ⟨p₀, (h₀.trans h₁).le⟩) (e.symm.lt_iff_lt.mpr h₀)
        (by simp [hm, h₁]) (algebraMap R (Localization.AtPrime p₂.1) x) <| by
          rw [← Localization.AtPrime.map_eq_maximalIdeal]
          exact mem_map_of_mem (algebraMap R (Localization.AtPrime p₂.1)) hx
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀_1 : p₀ < p₁
h₁_1 : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o
  (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm :
  Eq.{u_1 + 1} (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) (closedPoint (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₂ ⋯))
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq :
  Membership.mem (α := Localization.AtPrime p₂.asIdeal) q.asIdeal
    ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
      Localization.AtPrime p₂.asIdeal)
h₀ :
  (e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₀ ⋯) <
    q
h₁ : q.asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
have hxq₁ : Membership.mem (α := Localization.AtPrime p₂.asIdeal) (γ := Ideal (Localization.AtPrime p₂.asIdeal))
  (asIdeal
    ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      ((e :
          (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
            (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1))
        q)))
  ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
    Localization.AtPrime p₂.asIdeal)
Tactic: rw [← e.symm_apply_apply q] at h₀ h₁ hxq
Cleared hypotheses: hxq, h₀, h₁
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.LTSeries (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀_1 : p₀ < p₁
h₁_1 : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o
  (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) : Type u_1) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm :
  Eq.{u_1 + 1} (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) (closedPoint (Localization.AtPrime p₂.asIdeal))
    ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₂ ⋯))
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq :
  Membership.mem (α := Localization.AtPrime p₂.asIdeal) q.asIdeal
    ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
      Localization.AtPrime p₂.asIdeal)
h₀ :
  (e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ : PrimeSpectrum R }) p₀ ⋯) <
    q
h₁ : q.asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
hxq₁ :
  Membership.mem (α := Localization.AtPrime p₂.asIdeal) (γ := Ideal (Localization.AtPrime p₂.asIdeal))
    (asIdeal
      ((e.symm :
          (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1)) →
            PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
        ((e :
            (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
              (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) : Type u_1))
          q)))
    ((algebraMap R (Localization.AtPrime p₂.asIdeal) : (a : R) → Localization.AtPrime p₂.asIdeal) x :
      Localization.AtPrime p₂.asIdeal)
⊢ ∃ (q : PrimeSpectrum R), x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂
have h₂ : LT.lt (α := PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
  ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
        x ∈ Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry : PrimeSpectrum R }) p₀ sorry) :
    PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
  ((e.symm :
        (a : (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1)) →
          PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
      ((e :
          (a : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)) →
            (↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := sorry }) : Type u_1))
        q) :
    PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
Tactic: rw [← e.symm_apply_apply q] at h₀ h₁ hxq
Cleared hypotheses: hxq, h₀, h₁
-- 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
⊢ 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}))) =
  RelSeries.last (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}) p
Tactic: rw [show 0 = Fin.last p.length from Fin.zero_eq_mk.mpr hp, RelSeries.last]