-- Lean 4 proof step from Mathlib.Order.RelSeries (goal)
Goal:
α : Type u_3
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : WellFoundedGT α
n : ℕ
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))
have zero : ∀ (s : Fin (HAdd.hAdd (α := ℕ) 0 1) → α)
  (h :
    ∀ (i : Fin 0),
      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})
                0 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 := 0, toFun := s, step := h }.length + 1)) → Fin (t.length + 1)) =
        (RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              0 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 := 0, 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 := 0, 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})
                      0 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: induction n with
  | zero => exact ⟨⟨0, s, nofun⟩, (Equiv.refl _).toEmbedding, rfl, rfl, rfl⟩
  | succ n IH =>
    obtain ⟨t₁, i, ht, hi₁, hi₂⟩ := IH (s ∘ Fin.castSucc) fun _ ↦ h _
    obtain ⟨t₂, h₁, m, h₂, ht₂⟩ :=
      exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le (h (.last _)).le
    let t₃ : RelSeries {(a, b) : α × α | a ⋖ b} := ⟨m, (t₂ ·), fun i ↦ by simpa using ht₂ i⟩
    have H : t₁.last = t₂ 0 := (congr(t₁ $hi₂.symm).trans (congr_fun ht _)).trans h₁.symm
    refine ⟨t₁.smash t₃ H, ⟨Fin.snoc (Fin.castLE (by simp) ∘ i) (.last _), ?_⟩, ?_, ?_, ?_⟩
    · refine Fin.lastCases (Fin.lastCases (fun _ ↦ rfl) fun j eq ↦ ?_) fun j ↦ Fin.lastCases
        (fun eq ↦ ?_) fun k eq ↦ Fin.ext (congr_arg Fin.val (by simpa using eq) :)
      on_goal 2 => rw [eq_comm] at eq
      all_goals
        rw [Fin.snoc_castSucc] at eq
        obtain rfl : m = 0 := by simpa [t₃] using (congr_arg Fin.val eq).trans_lt (i j).2
        cases (h (.last _)).ne' (h₂.symm.trans h₁)
    · refine funext (Fin.lastCases ?_ fun j ↦ ?_)
      · convert! h₂; simpa using RelSeries.last_smash ..
      convert! congr_fun ht j using 1
      simp [RelSeries.smash_castLE]
    all_goals simp [Fin.snoc, Fin.castPred_zero, hi₁]
Cleared hypotheses: n, s, h