awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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
⊢ 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

Tactic:
simp_rw [show q = closedPoint R from PrimeSpectrum.ext hqm] at h

Premises used: PrimeSpectrum.ext
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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
⊢ 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₁ ⋯)))
    (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) ⋯)))

Tactic:
simpa using h₁
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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
⊢ 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

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₁))
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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

Tactic:
not_lt_zero (a := (e ⟨p₀, le_refl p₀⟩).1.height) (height_le_iff.mp hph _ inferInstance ?_)

Premises used: inferInstance, Ideal.height_le_iff, Iff.mp, not_lt_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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
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₀ ⋯)))
    (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₁ ⋯)))
⊢ False

Tactic:
refine not_lt_zero (a := (e ⟨p₀, le_refl p₀⟩).1.height) (height_le_iff.mp hph _ inferInstance ?_)

Premises used: inferInstance, Ideal.height_le_iff, Iff.mp, not_lt_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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
⊢ 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₀ ⋯)))
    (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₁ ⋯)))

Tactic:
simpa using h₀
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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
⊢ 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₂ ⋯))

Tactic:
have hm : closedPoint (Localization.AtPrime p₂.1) =
    e.symm ⟨p₂, le_refl p₂⟩ := (PrimeSpectrum.ext Localization.AtPrime.map_eq_maximalIdeal).symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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₂ ⋯))
⊢ LT.lt (α := PrimeSpectrum (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₁ ⋯) :
      PrimeSpectrum (Localization.AtPrime p₂.asIdeal))
    (closedPoint (Localization.AtPrime p₂.asIdeal) : PrimeSpectrum (Localization.AtPrime p₂.asIdeal))

Tactic:
simp [hm, h₁]
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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₂ ⋯))
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)
⊢ 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)

Tactic:
rw [← Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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))
    (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:
mem_map_of_mem (algebraMap R (Localization.AtPrime p₂.1)) hx

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Set.Mem, Localization.AtPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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))
    (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:
exact mem_map_of_mem (algebraMap R (Localization.AtPrime p₂.1)) hx

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Localization.AtPrime, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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₂ ⋯))
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 := ⋯ }) : 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₂
⊢ ∃ (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

Premises used: Iff.mpr, OrderIso.lt_iff_lt, OrderIso.symm, PrimeSpectrum.exist_mem_one_of_mem_maximal_ideal
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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)
⊢ 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)

Tactic:
rw [← e.symm_apply_apply q] at h₀ h₁ hxq

Premises used: OrderIso.symm_apply_apply
-- Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries
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)
⊢ LT.lt (α := PrimeSpectrum (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₀ ⋯) :
      PrimeSpectrum (Localization.AtPrime p₂.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) :
      PrimeSpectrum (Localization.AtPrime p₂.asIdeal))

Tactic:
rw [← e.symm_apply_apply q] at h₀ h₁ hxq

Premises used: OrderIso.symm_apply_apply