-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : WellFoundedGT α
n : ℕ
IH :
  ∀ (s : Fin (n + 1) → α)
    (h :
      ∀ (i : Fin n),
        Membership.mem (γ := SetRel α α)
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}
          (s i.castSucc, s i.succ)),
    ∃ (t :
      RelSeries (α := α)
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b})
      (i :
      Fin
          ((RelSeries.mk (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a < b})
                  n s h).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 ({ length := n, toFun := s, step := h }.length + 1)) → Fin (t.length + 1)) =
          (RelSeries.mk (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                n s h).toFun
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) ∧
        Eq (α :=
            Fin
              (t.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ⋖ b}) +
                1))
            ((i : (a : Fin ({ length := n, toFun := s, step := h }.length + 1)) → Fin (t.length + 1)) 0) 0 ∧
          Eq (α :=
            Fin
              (t.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ⋖ b}) +
                1))
            ((i : (a : Fin ({ length := n, toFun := s, step := h }.length + 1)) → Fin (t.length + 1))
                (Fin.last
                  ((RelSeries.mk (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a < b})
                        n s h).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))
s : Fin (n + 1 + 1) → α
h :
  ∀ (i : Fin (n + 1)),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (s i.castSucc, s i.succ)
t₁ :
  RelSeries (α := α)
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b}
i :
  Fin
      (RelSeries.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (RelSeries.mk (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            n (s ∘ Fin.castSucc) ⋯) +
        1) ↪
    Fin
      (t₁.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1)
ht :
  Eq (α :=
    Fin
        (RelSeries.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              n (s ∘ Fin.castSucc) ⋯) +
          1) →
      α)
    (t₁.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1)) → Fin (t₁.length + 1)))
    (RelSeries.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (RelSeries.mk (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        n (s ∘ Fin.castSucc) ⋯))
hi₁ :
  Eq (α :=
    Fin
      (t₁.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a ⋖ b}) +
        1))
    ((i : (a : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.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 ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1)) → Fin (t₁.length + 1))
        (Fin.last
          (RelSeries.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              n (s ∘ Fin.castSucc) ⋯))) :
      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))
t₂ : ℕ → α
h₁ : t₂ 0 = s (Fin.last n).castSucc
m : ℕ
h₂ : t₂ m = s (Fin.last n).succ
ht₂ : ∀ i < m, t₂ i ⋖ t₂ (i + 1)
t₃ : RelSeries (α := α)
  {x : α × α |
    match (motive := α × α → Prop) x with
    | (a, b) => a ⋖ b} :=
  RelSeries.mk (r :=
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ⋖ b})
    m (fun (x : Fin (m + 1)) ↦ t₂ (↑x : ℕ)) ⋯
H :
  t₁.last (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ⋖ b}) =
    t₂ 0
succ :
  Function.comp (α :=
      Fin
        ((RelSeries.mk (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b})
                (n + 1) s h).length
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))
      ((t₁.smash (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b})
            t₃ H).toFun
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}))
      (⇑{
            toFun :=
              Fin.snoc (α :=
                fun
                  (a :
                    Fin
                      ((RelSeries.mk (r :=
                              {x : α × α |
                                match (motive := α × α → Prop) x with
                                | (a, b) => a < b})
                              (n + 1) s h).length
                          (r :=
                          {x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a < b}) +
                        1)) ↦
                Fin
                  ((t₁.smash (r :=
                          {x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a ⋖ b})
                          t₃ H).length
                      (r :=
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ⋖ b}) +
                    1))
                (Fin.castLE ⋯ ∘
                  (⇑i :
                    (a : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1)) → Fin (t₁.length + 1)))
                (Fin.last
                  ((t₁.smash (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ⋖ b})
                        t₃ H).length
                    (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a ⋖ b}))),
            inj' := ⋯ :
            Fin
                ((RelSeries.mk (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a < b})
                        (n + 1) s h).length
                    (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b}) +
                  1) ↪
              Fin
                ((t₁.smash (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ⋖ b})
                        t₃ H).length
                    (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a ⋖ b}) +
                  1) } :
        (a : Fin ({ length := n + 1, toFun := s, step := h }.length + 1)) → Fin ((t₁.smash t₃ H).length + 1))
      (Fin.last
        ((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (n + 1) s h).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}))) =
    (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (n + 1) s h).toFun
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      (Fin.last
        ((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (n + 1) s h).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})))
succ₁ :
  ∀
    (j :
      Fin
        ((RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              (n + 1) s h).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}))),
    ((t₁.smash (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b})
                t₃ H).toFun
            (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) ∘
          (⇑{
                toFun :=
                  Fin.snoc (α :=
                    fun
                      (a :
                        Fin
                          ((RelSeries.mk (r :=
                                  {x : α × α |
                                    match (motive := α × α → Prop) x with
                                    | (a, b) => a < b})
                                  (n + 1) s h).length
                              (r :=
                              {x : α × α |
                                match (motive := α × α → Prop) x with
                                | (a, b) => a < b}) +
                            1)) ↦
                    Fin
                      ((t₁.smash (r :=
                              {x : α × α |
                                match (motive := α × α → Prop) x with
                                | (a, b) => a ⋖ b})
                              t₃ H).length
                          (r :=
                          {x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a ⋖ b}) +
                        1))
                    (Fin.castLE ⋯ ∘
                      (⇑i :
                        (a : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1)) →
                          Fin (t₁.length + 1)))
                    (Fin.last
                      ((t₁.smash (r :=
                            {x : α × α |
                              match (motive := α × α → Prop) x with
                              | (a, b) => a ⋖ b})
                            t₃ H).length
                        (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ⋖ b}))),
                inj' := ⋯ :
                Fin
                    ((RelSeries.mk (r :=
                            {x : α × α |
                              match (motive := α × α → Prop) x with
                              | (a, b) => a < b})
                            (n + 1) s h).length
                        (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a < b}) +
                      1) ↪
                  Fin
                    ((t₁.smash (r :=
                            {x : α × α |
                              match (motive := α × α → Prop) x with
                              | (a, b) => a ⋖ b})
                            t₃ H).length
                        (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ⋖ b}) +
                      1) } :
            (a : Fin ({ length := n + 1, toFun := s, step := h }.length + 1)) → Fin ((t₁.smash t₃ H).length + 1)))
        j.castSucc =
      (RelSeries.mk (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b})
            (n + 1) s h).toFun
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        j.castSucc
⊢ (t₁.smash (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b})
            t₃ H).toFun
        (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑{
            toFun :=
              Fin.snoc (α :=
                fun
                  (a :
                    Fin
                      ((RelSeries.mk (r :=
                              {x : α × α |
                                match (motive := α × α → Prop) x with
                                | (a, b) => a < b})
                              (n + 1) s h).length
                          (r :=
                          {x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a < b}) +
                        1)) ↦
                Fin
                  ((t₁.smash (r :=
                          {x : α × α |
                            match (motive := α × α → Prop) x with
                            | (a, b) => a ⋖ b})
                          t₃ H).length
                      (r :=
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ⋖ b}) +
                    1))
                (Fin.castLE ⋯ ∘
                  (⇑i :
                    (a : Fin ({ length := n, toFun := s ∘ Fin.castSucc, step := ⋯ }.length + 1)) → Fin (t₁.length + 1)))
                (Fin.last
                  ((t₁.smash (r :=
                        {x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ⋖ b})
                        t₃ H).length
                    (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a ⋖ b}))),
            inj' := ⋯ } :
        (a : Fin ({ length := n + 1, toFun := s, step := h }.length + 1)) → Fin ((t₁.smash t₃ H).length + 1)) =
    (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          (n + 1) s h).toFun
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})

Tactic:
refine funext (Fin.lastCases ?_ fun j ↦ ?_)

Premises used: Fin.lastCases, funext