-- 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
inl :
  ∀
    (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),
    ∃ (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
inr :
  ∀
    (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),
    ∃ (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 hlt | rfl := lt_or_eq_of_le hm

Premises used: lt_or_eq_of_le, rfl