-- 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 =
    ⊥
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)
hit :
  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})
hi₁ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1)) 0) 0
hi₂ :
  Eq (α :=
    Fin
      (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}))) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
    (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b})) :
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
refine_2 :
  t.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s
refine_2₁ :
  t.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
      (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}))) =
    RelSeries.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      s
refine_2₂ :
  t.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
      (Fin.last
        (t.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}))) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})))
refine_2₃ :
  t.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
      ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})))) =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})))
refine_2₄ :
  t.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b})
      ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
        (Fin.last
          (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})))) =
    Function.comp (α :=
      Fin
        (s.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))
      (Fin.last
        (s.length (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 refine_2₅ : t.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b})
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
      (Fin.last
        (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})))) =
  t.toFun (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b})
    ((i : (a : Fin (s.length + 1)) → Fin (t.length + 1))
      (Fin.last
        (s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}))))
Tactic: rw [← h₂, RelSeries.last, RelSeries.last, ← hi₂, ← hit, Function.comp]