-- Lean 4 proof step from Mathlib.Order.KrullDimension (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
n : ℕ∞
h :
  ∀ (p : LTSeries α),
    RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          p =
        a →
      (↑(p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) ≤
        n
p : LTSeries α
hlast :
  RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      p ≤
    a
inr :
  ∀
    (this :
      ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞}
        (h :
          ∀ (p : LTSeries α),
            RelSeries.last (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b})
                  p =
                a →
              (↑(p.length (r :=
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a < b})) :
                  ℕ∞) ≤
                n)
        ⦃p : LTSeries α⦄
        (hlast :
          RelSeries.last (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              p ≤
            a)
        (hlenpos :
          p.length (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) ≠
            0),
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n)
    (hlenpos :
      ¬p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) ≠
          0),
    (↑(p.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞) ≤
      n
⊢ (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
have wlog : ∀ {α : Type u_1} [inst : Preorder α] {a : α} {n : ℕ∞}
  (h :
    ∀ (p : LTSeries α),
      RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            p =
          a →
        (↑(p.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})) :
            ℕ∞) ≤
          n)
  ⦃p : LTSeries α⦄
  (hlast :
    RelSeries.last (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        p ≤
      a)
  (hlenpos :
    p.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) ≠
      0),
  (↑(p.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) ≤
    n
Tactic: wlog hlenpos : p.length ≠ 0
Cleared hypotheses: a, n, h, p, hlast