-- 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)
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
⊢ ∃ (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}) ≤
    (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 := sorry : PrimeSpectrum R } sorry)
          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 := sorry : PrimeSpectrum R } sorry)
                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: use q.snoc ⟨⟨m, inferInstance⟩, mem_support_mono hm q.last.2⟩ hlt