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