awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
q : LTSeries (↑(support R M) : Type u_1)
obtain :
  ∀ (m : Ideal R) (hmm : m.IsMaximal)
    (hm :
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                q) :
            PrimeSpectrum R).asIdeal ≤
        m),
    ∃ (p : LTSeries (↑(support R M) : Type u_1)),
      q.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b}) ≤
          p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b}) ∧
        (↑(RelSeries.last (r :=
                  {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                    match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                    | (a, b) => a < b})
                  p) :
              PrimeSpectrum R).asIdeal.IsMaximal
⊢ ∃ (p : LTSeries (↑(support R M) : Type u_1)),
    q.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ∧
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal.IsMaximal

Tactic:
obtain ⟨m, hmm, hm⟩ := exists_le_maximal _ q.last.1.2.1

Premises used: Ideal.exists_le_maximal, Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
q : LTSeries (↑(support R M) : Type u_1)
m : Ideal R
hmm : m.IsMaximal
hm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal ≤
    m
hlt :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal <
    m
⊢ q.length (r :=
        {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
          match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
          | (a, b) => a < b}) ≤
      (RelSeries.snoc (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q
            (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
              { asIdeal := m, isPrime := ⋯ : PrimeSpectrum R } ⋯)
            hlt).length
        (r :=
        {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
          match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
          | (a, b) => a < b}) ∧
    (↑((RelSeries.snoc (r :=
                  {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                    match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                    | (a, b) => a < b})
                  q
                  (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦
                    Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
                    { asIdeal := m, isPrime := ⋯ : PrimeSpectrum R } ⋯)
                  hlt).last
              (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b})) :
          PrimeSpectrum R).asIdeal.IsMaximal

Tactic:
simpa
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
q : LTSeries (↑(support R M) : Type u_1)
hmm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal.IsMaximal
hm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal ≤
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            q) :
        PrimeSpectrum R).asIdeal
w : LTSeries (↑(support R M) : Type u_1)
h :
  q.length (r :=
        {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
          match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
          | (a, b) => a < b}) ≤
      q.length (r :=
        {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
          match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
          | (a, b) => a < b}) ∧
    (↑(RelSeries.last (r :=
              {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                | (a, b) => a < b})
              q) :
          PrimeSpectrum R).asIdeal.IsMaximal
⊢ ∃ (p : LTSeries (↑(support R M) : Type u_1)),
    q.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ∧
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal.IsMaximal

Tactic:
use q
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
⊢ supportDim R M ≤ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
iSup_le_iff.mpr (fun p ↦ ?_)

Premises used: Iff.mpr, Order.krullDim, Module.supportDim, iSup_le_iff
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
refine :
  ∀ (p : LTSeries (↑(support R M) : Type u_1)),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
⊢ supportDim R M ≤ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
refine iSup_le_iff.mpr (fun p ↦ ?_)

Premises used: Iff.mpr, iSup_le_iff
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
p : LTSeries (↑(support R M) : Type u_1)
inr :
  ∀
    (this :
      ∀ (p : LTSeries (↑(support R M) : Type u_1))
        (hxp :
          x ∈
            (↑(RelSeries.last (r :=
                    {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                      match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                      | (a, b) => a < b})
                    p) :
                PrimeSpectrum R).asIdeal),
        (↑(p.length (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})) :
            WithBot ℕ∞) ≤
          supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1)
    (hxp :
      x ∉
        (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
wlog :
  ∀ (p : LTSeries (↑(support R M) : Type u_1))
    (hxp :
      x ∈
        (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
⊢ (↑(p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞) ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
wlog hxp : x ∈ p.last.1.1 generalizing p

Premises used: RelSeries.last, Subtype.val, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
p : LTSeries (↑(support R M) : Type u_1)
this :
  ∀ (p : LTSeries (↑(support R M) : Type u_1))
    (hxp :
      x ∈
        (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
hxp :
  x ∉
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal
inr :
  ∀ (p_1 : LTSeries (↑(support R M) : Type u_1))
    (hle :
      p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}) ≤
        p_1.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b}))
    (hm :
      (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p_1) :
            PrimeSpectrum R).asIdeal.IsMaximal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
⊢ (↑(p.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞) ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
obtain ⟨p, hle, hm⟩ := exists_ltSeries_support_isMaximal_last_of_ltSeries_support p

Premises used: Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
p_1 : LTSeries (↑(support R M) : Type u_1)
this :
  ∀ (p : LTSeries (↑(support R M) : Type u_1))
    (hxp :
      x ∈
        (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
hxp :
  x ∉
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p_1) :
        PrimeSpectrum R).asIdeal
p : LTSeries (↑(support R M) : Type u_1)
hle :
  p_1.length (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b}) ≤
    p.length (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b})
hm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal.IsMaximal
⊢ Ideal.jacobson (annihilator R M) ≤
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal

Tactic:
have hj : (annihilator R M).jacobson ≤ p.last.1.1 :=
      sInf_le ⟨mem_support_iff_of_finite.mp p.last.2, inferInstance⟩
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
p_1 : LTSeries (↑(support R M) : Type u_1)
this :
  ∀ (p : LTSeries (↑(support R M) : Type u_1))
    (hxp :
      x ∈
        (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
hxp :
  x ∉
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p_1) :
        PrimeSpectrum R).asIdeal
p : LTSeries (↑(support R M) : Type u_1)
hle :
  p_1.length (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b}) ≤
    p.length (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b})
hm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal.IsMaximal
hj :
  Ideal.jacobson (annihilator R M) ≤
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal
⊢ (↑(p_1.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞) ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
(Nat.cast_le.mpr hle).trans <| this _ (hj h)

Premises used: Iff.mpr, Nat.cast_le, LE.le.trans
-- Module: Mathlib.RingTheory.KrullDimension.Regular
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
M : Type u_2
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
x : R
h : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
h_1 : Nontrivial M
p_1 : LTSeries (↑(support R M) : Type u_1)
this :
  ∀ (p : LTSeries (↑(support R M) : Type u_1))
    (hxp :
      x ∈
        (↑(RelSeries.last (r :=
                {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
                  match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
                  | (a, b) => a < b})
                p) :
            PrimeSpectrum R).asIdeal),
    (↑(p.length (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})) :
        WithBot ℕ∞) ≤
      supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
hxp :
  x ∉
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p_1) :
        PrimeSpectrum R).asIdeal
p : LTSeries (↑(support R M) : Type u_1)
hle :
  p_1.length (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b}) ≤
    p.length (r :=
      {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
        match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
        | (a, b) => a < b})
hm :
  (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal.IsMaximal
hj :
  Ideal.jacobson (annihilator R M) ≤
    (↑(RelSeries.last (r :=
            {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
              match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
              | (a, b) => a < b})
            p) :
        PrimeSpectrum R).asIdeal
⊢ (↑(p_1.length (r :=
          {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) |
            match (motive := (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) → Prop) x with
            | (a, b) => a < b})) :
      WithBot ℕ∞) ≤
    supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1

Tactic:
exact (Nat.cast_le.mpr hle).trans <| this _ (hj h)

Premises used: Iff.mpr, Nat.cast_le, LE.le.trans