-- 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)
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 :
      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 + 1) 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 + 1, toFun := s, step := h }.length + 1)) → Fin (t.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}) ∧
        Eq (α :=
            Fin
              (t.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ⋖ b}) +
                1))
            ((i : (a : Fin ({ length := n + 1, 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 + 1, 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 + 1) 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))
⊢ ∃ (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 + 1) 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 + 1, toFun := s, step := h }.length + 1)) → Fin (t.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}) ∧
      Eq (α :=
          Fin
            (t.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ⋖ b}) +
              1))
          ((i : (a : Fin ({ length := n + 1, 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 + 1, 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 + 1) 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))

Tactic:
obtain ⟨t₁, i, ht, hi₁, hi₂⟩ := IH (s ∘ Fin.castSucc) fun _ ↦ h _

Premises used: Function.comp, Fin.castSucc