mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : 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 := ⋯ }) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm : closedPoint (Localization.AtPrime p₂.asIdeal) = e.symm ⟨p₂, ⋯⟩
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq : (algebraMap R (Localization.AtPrime p₂.asIdeal)) x ∈ (e.symm (e q)).asIdeal
h₀ : e.symm ⟨p₀, ⋯⟩ < e.symm (e q)
h₁ : (e.symm (e q)).asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
⊢ ↑(e q) < p₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
a✝ : Nontrivial M
p : LTSeries ↑(support R M)
hxp : x ∈ (↑(RelSeries.last p)).asIdeal
q : LTSeries (PrimeSpectrum R)
hxq : x ∈ (q.toFun 1).asIdeal
hq : (p.map Subtype.val ⋯).length = q.length
h0 : ↑(RelSeries.head p) = RelSeries.head q
right✝ : RelSeries.last (p.map Subtype.val ⋯) = RelSeries.last q
hp0 : ¬p.length = 0
⊢ ∀ (i : Fin (p.length - 1)),
    (match i.castSucc with
        | ⟨i, hi⟩ =>
          have hi := ⋯;
          ⟨q.toFun ⟨i + 1, hi⟩, ⋯⟩,
        match i.succ with
        | ⟨i, hi⟩ =>
          have hi := ⋯;
          ⟨q.toFun ⟨i + 1, hi⟩, ⋯⟩) ∈
      {(a, b) | a < b}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
h : P.height ≤ ↑t.card
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
⊢ span ↑t = map (algebraMap R S) (span ↑s) ⊔ span ↑o

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsNoetherianRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
h : x ∈ (annihilator R M).jacobson
⊢ supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : n = 0
⊢ 1 = Fin.last p.length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
⊢ (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
⊢ p.length.sub 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
⊢ p.length.sub 0 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
⊢ (RelSeries.smash lp' l' hlp').length = lp.length + lq.length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
⊢ x ∈ ((RelSeries.eraseLast p).eraseLast.snoc q h2).last.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
⊢ ((RelSeries.eraseLast p).eraseLast.snoc q h2).length = n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
⊢ 1 = Fin.castSucc 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsNoetherianRing R
S : Type u_2
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsNoetherianRing S
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ P.height = p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ (RelSeries.last Q, RelSeries.last p) ∈ {(a, b) | a < b}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
⊢ support R (QuotSMulTop x M) ⊆ support R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ x ∈ ((RelSeries.snoc Q (RelSeries.last p) ⋯).toFun 1).asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ n + 1 = (RelSeries.snoc Q (RelSeries.last p) ⋯).length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ RelSeries.head p = (RelSeries.snoc Q (RelSeries.last p) ⋯).head

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ RelSeries.last p = (RelSeries.snoc Q (RelSeries.last p) ⋯).last

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
le : support R (QuotSMulTop x M) ⊆ support R M
q : LTSeries ↑(support R M) := p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) ⋯
r✝ : Ideal R
hrm : r✝ ∈ (annihilator R M).minimalPrimes
hr : r✝ ≤ (↑(RelSeries.head q)).asIdeal
r : ↑(support R M) := ⟨{ asIdeal := r✝, isPrime := ⋯ }, ⋯⟩
h : r = RelSeries.head q
⊢ (↑(RelSeries.head q)).asIdeal ∈ (annihilator R M).minimalPrimes

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : LTSeries (PrimeSpectrum R)
x : R
hx : x ∈ (RelSeries.last p).asIdeal
⊢ ∃ q,
    x ∈ (q.toFun 1).asIdeal ∧
      p.length = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
le : support R (QuotSMulTop x M) ⊆ support R M
q : LTSeries ↑(support R M) := p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) ⋯
r✝ : Ideal R
hrm : r✝ ∈ (annihilator R M).minimalPrimes
hr✝ : r✝ ≤ (↑(RelSeries.head q)).asIdeal
r : ↑(support R M) := ⟨{ asIdeal := r✝, isPrime := ⋯ }, ⋯⟩
hr : r < RelSeries.head q
⊢ ↑p.length + 1 = ↑(RelSeries.cons q r hr).length

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
⊢ supportDim R (QuotSMulTop x M) + 1 ≤ supportDim R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ Ring.jacobson R
⊢ ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ Ring.jacobson R
⊢ span {x} = x • ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
⊢ ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ Ring.jacobson R
⊢ ringKrullDim (R ⧸ span {x}) + 1 = ringKrullDim R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
hr : r ∈ nonZeroDivisors R
p : Ideal R
inst✝ : p.IsPrime
h : ↑p.height = ringKrullDim R
hp : r ∈ p
⊢ ringKrullDim (R ⧸ span {r}) + 1 = ringKrullDim R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
hx : x ∈ maximalIdeal R
⊢ ringKrullDim R ≤ ringKrullDim (R ⧸ x • ⊤) + 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
S : Finset R
hS : ↑S ⊆ ↑(maximalIdeal R)
⊢ ringKrullDim R ≤ ringKrullDim (R ⧸ span ↑S) + ↑S.card

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
h : I ≠ ⊤
⊢ ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ maximalIdeal R
⊢ x ∈ Ring.jacobson R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M],
    Sequence.IsRegular M rs' → supportDim R (M ⧸ ofList rs' • ⊤) + ↑rs'.length = supportDim R M
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
isu : IsUnit x
⊢ ⊤ = ofList (x :: rs') • ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
inst✝³ : IsLocalRing R
x : R
rs' : List R
ih :
  ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module R M] [Module.Finite R M],
    Sequence.IsRegular M rs' → supportDim R (M ⧸ ofList rs' • ⊤) + ↑rs'.length = supportDim R M
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
reg : Sequence.IsRegular M (x :: rs')
⊢ x ∈ maximalIdeal R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsNoetherianRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular M rs
⊢ supportDim R (M ⧸ ofList rs • ⊤) + ↑rs.length = supportDim R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ofList rs = ofList rs • ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
J : Submodule R M
hJ : J ∈ s
⊢ ∀ ⦃y : Submodule R M⦄,
    y ∈ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical} →
      ((id y).colon Set.univ).radical = ((id J).colon Set.univ).radical

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ringKrullDim (R ⧸ ofList rs) + ↑rs.length = ringKrullDim R

Tactic:
by

Goal state after: