-- 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 =
    ⊥
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}) =
          ⊤
have inr : ∀
  (t :
    RelSeries (α := α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
  (i :
    Fin
        ((RelSeries.snoc (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                s ⊤ sorry).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))
  (hi :
    t.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) ∘
        (⇑i : (a : Fin ((RelSeries.snoc s ⊤ sorry).length + 1)) → Fin (t.length + 1)) =
      (RelSeries.snoc (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            s ⊤ sorry).toFun
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}))
  (ht :
    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}) =
        ⊤),
  ∃ (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: obtain ⟨t, i, hi, ht⟩ := this (s.snoc ⊤ (lt_top_iff_ne_top.mpr h₂)) (by simp [h₁]) (by simp)