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
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)
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})) : ℕ∞))
⊢ 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:
apply WithBot.coe_le_coe.mpr

Premises used: Iff.mpr, WithBot.coe_le_coe
-- 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
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)
simp :
  ∀ (i : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)),
    HAdd.hAdd (α := ℕ∞)
        (↑(i.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})) : ℕ∞)
⊢ 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:
simp only [ENat.iSup_add, iSup_le_iff]

Premises used: ENat.iSup_add, iSup_le_iff
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M))
    (↑(RelSeries.head (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) |
            match (motive :=
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) →
                Prop)
              x_1 with
            | (a, b) => a < b})
          p) :
      PrimeSpectrum R)

Tactic:
have hp := p.head.2
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M))
    (↑(RelSeries.head (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) |
            match (motive :=
              (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) ×
                  (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1) →
                Prop)
              x_1 with
            | (a, b) => a < b})
          p) :
      PrimeSpectrum R)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)

Tactic:
simp only [support_quotSMulTop, Set.mem_inter_iff, mem_zeroLocus, Set.singleton_subset_iff] at hp

Premises used: Set.singleton_subset_iff, Set.mem_inter_iff, PrimeSpectrum.mem_zeroLocus, Module.support_quotSMulTop
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)

Tactic:
simp
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)

Tactic:
have le : support R (QuotSMulTop x M) ⊆ support R M := by simp
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
obtain :
  ∀ (r : Ideal R) (hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r)
    (hr :
      r ≤
        (↑(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})
                q) :
            PrimeSpectrum R).asIdeal),
    HAdd.hAdd (α := ℕ∞)
        (↑(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})) : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(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:
obtain ⟨r, hrm, hr⟩ := exists_minimalPrimes_le (mem_support_iff_of_finite.mp q.head.2)

Premises used: Module.mem_support_iff_of_finite, Ideal.exists_minimalPrimes_le, Iff.mp, RelSeries.head, Subtype.property
-- 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
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_1 : Nontrivial M
h_2 : 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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
r_1 : Ideal R
hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r_1
hr :
  r_1 ≤
    (↑(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})
            q) :
        PrimeSpectrum R).asIdeal
r : (↑(support R M) : Type u_1) :=
  Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
    { asIdeal := r_1, isPrime := ⋯ } ⋯
h :
  r =
    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})
      q
rwa rwa₁ rwa₂ rwa₃ :
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) (↑r : PrimeSpectrum R).asIdeal
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M))
    (↑(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})
            q) :
        PrimeSpectrum R).asIdeal

Tactic:
rwa [← h]
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
r_1 : Ideal R
hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r_1
hr :
  r_1 ≤
    (↑(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})
            q) :
        PrimeSpectrum R).asIdeal
r : (↑(support R M) : Type u_1) :=
  Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
    { asIdeal := r_1, isPrime := ⋯ } ⋯
⊢ r <
    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})
      q

Tactic:
have hr : r < q.head := lt_of_le_of_ne hr (fun h ↦ hn q.head.1.1 (by rwa [← h]) hp.2)
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
r_1 : Ideal R
hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r_1
hr_1 :
  r_1 ≤
    (↑(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})
            q) :
        PrimeSpectrum R).asIdeal
r : (↑(support R M) : Type u_1) :=
  Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
    { asIdeal := r_1, isPrime := ⋯ } ⋯
hr :
  r <
    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})
      q
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(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 =
    (↑((RelSeries.cons (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 r hr).length
          (r := {x : (↑(support R M) : Type u_1) × (↑(support R M) : Type u_1) | x.1 < x.2})) :
      ℕ∞)

Tactic:
simp [q]
-- 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
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)
p : LTSeries (↑(support.{u_1, u_2} R (QuotSMulTop x M)) : Type u_1)
hp :
  Membership.mem (γ := Set (PrimeSpectrum R)) (support R M)
      (↑(RelSeries.head (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})
            p) :
        PrimeSpectrum R) ∧
    x ∈
      (↑(↑(RelSeries.head (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})
                  p) :
              PrimeSpectrum R).asIdeal :
        Set R)
le : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M)
q : LTSeries (↑(support R M) : Type u_1) :=
  p.map (Set.MapsTo.restrict id (support.{u_1, u_2} R (QuotSMulTop x M)) (support R M) le) ⋯
r_1 : Ideal R
hrm : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) r_1
hr_1 :
  r_1 ≤
    (↑(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})
            q) :
        PrimeSpectrum R).asIdeal
r : (↑(support R M) : Type u_1) :=
  Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) x)
    { asIdeal := r_1, isPrime := ⋯ } ⋯
hr :
  r <
    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})
      q
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(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:
exact le_of_eq_of_le (by simp [q]) (le_iSup _ (q.cons r hr))

Premises used: le_iSup, le_of_eq_of_le, RelSeries.cons
-- 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
hn : ∀ (p : Ideal R), Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (annihilator R M)) p → x ∉ p
hx : Membership.mem (γ := Ideal R) (Ideal.jacobson (annihilator R M)) x
⊢ supportDim.{u_1, u_2} R (QuotSMulTop x M) + 1 = supportDim R M

Tactic:
le_antisymm (supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes hn)
    (supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson hx)

Premises used: le_antisymm, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes