-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : WellFoundedLT α
inst_3 : WellFoundedGT α
s : LTSeries α
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 =
        ⊥),
    ∃ (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.head (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
      ((RelSeries.cons (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              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)
hi :
  t.toFun (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a ⋖ b}) ∘
      (⇑i : (a : Fin ((RelSeries.cons s ⊥ ⋯).length + 1)) → Fin (t.length + 1)) =
    (RelSeries.cons (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          s ⊥ ⋯).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}) =
      ⊤
x x_1 :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
⊢ Eq (α :=
      Fin
        (t.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a ⋖ b}) +
          1))
      ((fun
            (j :
              Fin
                (s.length (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b}) +
                  1)) ↦
          ((i : (a : Fin ((RelSeries.cons s ⊥ ⋯).length + 1)) → Fin (t.length + 1)) (Fin.cast ⋯ j.succ) :
            Fin
              (t.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ⋖ b}) +
                1)))
        x)
      ((fun
            (j :
              Fin
                (s.length (r :=
                    {x : α × α |
                      match (motive := α × α → Prop) x with
                      | (a, b) => a < b}) +
                  1)) ↦
          ((i : (a : Fin ((RelSeries.cons s ⊥ ⋯).length + 1)) → Fin (t.length + 1)) (Fin.cast ⋯ j.succ) :
            Fin
              (t.length (r :=
                  {x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ⋖ b}) +
                1)))
        x_1) →
    x = x_1

Tactic:
simp