-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
h₁ :
  RelSeries.head (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s =
    ⊥
⊢ ∃ (t :
    RelSeries (α := α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
    (i :
    Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1) ↪
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1)),
    t.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) ∘
          (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
        s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ∧
      t.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) =
          ⊥ ∧
        t.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) =
          ⊤
have inr : ∀
  (this :
    ∀ {α : Type u_3} [inst : PartialOrder α] [inst_4 : BoundedOrder α] [WellFoundedLT α] [WellFoundedGT α]
      (s : LTSeries α)
      (h₁ :
        RelSeries.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            s =
          ⊥)
      (h₂ :
        RelSeries.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            s =
          ⊤),
      ∃ (t :
        RelSeries (α := α)
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})
        (i :
        Fin
            (s.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1) ↪
          Fin
            (t.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) +
              1)),
        t.toFun (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) ∘
              (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
            s.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b}) ∧
          t.head (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) =
              ⊥ ∧
            t.last (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) =
              ⊤)
  (h₂ :
    ¬RelSeries.last (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          s =
        ⊤),
  ∃ (t :
    RelSeries (α := α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
    (i :
    Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1) ↪
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1)),
    t.toFun (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) ∘
          (⇑i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) =
        s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) ∧
      t.head (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) =
          ⊥ ∧
        t.last (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) =
          ⊤
Tactic: wlog h₂ : s.last = ⊤