awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
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)
⊢ ∃ (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
have 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
Tactic: use q
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
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
⊢ supportDim R M ≤ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
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
have 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
Tactic: refine iSup_le_iff.mpr (fun p ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
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)
⊢ (↑(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
have 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
Tactic: wlog hxp : x ∈ p.last.1.1 generalizing p
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
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
⊢ (↑(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
have 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
Tactic: wlog hxp : x ∈ p.last.1.1 generalizing p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
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
⊢ (↑(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
have 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
Tactic: obtain ⟨p, hle, hm⟩ := exists_ltSeries_support_isMaximal_last_of_ltSeries_support p
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
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
⊢ (↑(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
have 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
Tactic: have hj : (annihilator R M).jacobson ≤ p.last.1.1 :=
      sInf_le ⟨mem_support_iff_of_finite.mp p.last.2, inferInstance⟩
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
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)
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
q : LTSeries (PrimeSpectrum R)
hxq :
  x ∈
    (q.toFun (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        1).asIdeal
hq :
  RelSeries.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      (p.map
        (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x))
        ⋯) =
    q.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
h0 :
  (↑(RelSeries.head (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) =
    RelSeries.head (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      q
right :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      (p.map
        (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x))
        ⋯) =
    RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      q
hp0 :
  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}) =
    0
hb : supportDim.{u_1, u_2} R (QuotSMulTop x M) ≠ ⊥
⊢ (↑(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
have pos : (↑0 : WithBot ℕ∞) ≤ (↑((supportDim.{u_1, u_2} R (QuotSMulTop x M)).unbot hb) : WithBot ℕ∞) + 1
Tactic: rw [hp0, ← WithBot.coe_unbot (supportDim R (QuotSMulTop x M)) hb]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 ≤ supportDim R M
have a : Nontrivial M
Tactic: nontriviality M
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 ≤ supportDim R M
have a : Nontrivial.{u_2} (QuotSMulTop x M)
Tactic: nontriviality (QuotSMulTop x M)
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 ≤ supportDim R M
have this : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
Tactic: have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 ≤ supportDim R M
have this₁ : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
Tactic: have : Nonempty (Module.support R (QuotSMulTop x M)) := nonempty_support_of_nontrivial.to_subtype
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 ≤ supportDim R M
have simp : HAdd.hAdd (α := WithBot ℕ∞)
    (↑(⨆ (p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
          (↑(p.length (r :=
                {x_1 :
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                  x_1.1 < x_1.2})) :
            ℕ∞)) :
      WithBot ℕ∞)
    1 ≤
  (↑(⨆ (p : LTSeries (↑(support R M) : Type u_1)),
        (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)) :
    WithBot ℕ∞)
Tactic: simp only [supportDim, Order.krullDim_eq_iSup_length]
-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.Regular (goal)
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
h : Nontrivial M
h_1 : Nontrivial.{u_2} (QuotSMulTop x M)
this_1 : Nonempty.{u_1 + 1} (↑(support R M) : Type u_1)
this : Nonempty.{u_1 + 1} (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
⊢ HAdd.hAdd (α := WithBot ℕ∞)
      (↑(⨆ (p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
            (↑(p.length (r :=
                  {x_1 :
                    (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                      (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
                    x_1.1 < x_1.2})) :
              ℕ∞)) :
        WithBot ℕ∞)
      1 ≤
    (↑(⨆ (p : LTSeries (↑(support R M) : Type u_1)),
          (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞)) :
      WithBot ℕ∞)
have apply : LE.le (α := ℕ∞)
  ((fun (x1 x2 : ℕ∞) ↦ x1 + x2)
    (⨆ (p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
      (↑(p.length (r :=
            {x_1 :
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) |
              x_1.1 < x_1.2})) :
        ℕ∞))
    1)
  (⨆ (p : LTSeries (↑(support R M) : Type u_1)),
    (↑(p.length (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) : ℕ∞))
Tactic: apply WithBot.coe_le_coe.mpr