-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem mergeSortTR₂_run'_eq_mergeSort : {n : Nat} → (l : { l : List α // l.length = n }) → (w : l' = l.1.reverse) → mergeSortTR₂.run' le l = mergeSort l' le
  | 0, ⟨[], _⟩, w
  | 1, ⟨[a], _⟩, w => by simp_all [mergeSortTR₂.run', mergeSort]
  | n+2, ⟨a :: b :: l, h⟩, w => by
    cases h
    simp only [mergeSortTR₂.run', mergeSort]
    rw [splitRevInTwo'_fst, splitRevInTwo'_snd]
    rw [mergeSortTR₂_run_eq_mergeSort, mergeSortTR₂_run'_eq_mergeSort _ rfl]
    rw [← merge_eq_mergeTR]
    have w' := congrArg length w
    simp at w'
    cases l' with
    | nil => simp at w'
    | cons x l' =>
      cases l' with
      | nil => simp at w'
      | cons y l' =>
        rw [mergeSort]
        congr 2
        · dsimp at w
          simp only [w]
          simp only [splitInTwo_fst, splitInTwo_snd, reverse_take, take_reverse]
          congr 1
          rw [w, length_reverse]
          simp
        · dsimp at w
          simp only [w]
          simp only [reverse_cons, append_assoc, singleton_append, splitInTwo_snd, length_cons]
          congr 1
          simp at w'
          omega
termination_by n => n

Proof state:
case refl.cons.cons.e_xs.e_xs
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = (a :: b :: l).reverse
w' : (x :: y :: l').length = l.length + 2
⊢ (drop ((a :: b :: l).length - (l.length + 2 + 1) / 2) (a :: b :: l)).reverse.reverse.reverse =
    (drop ((a :: b :: l).length - ((x :: y :: l').length + 1) / 2) (a :: b :: l)).reverse

Tactic:
congr 1

Result:
case refl.cons.cons.e_xs.e_xs.e_as
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = (a :: b :: l).reverse
w' : (x :: y :: l').length = l.length + 2
⊢ (drop ((a :: b :: l).length - (l.length + 2 + 1) / 2) (a :: b :: l)).reverse.reverse =
    drop ((a :: b :: l).length - ((x :: y :: l').length + 1) / 2) (a :: b :: l)

Proof state:
α : Type u_1
l' : List α
le : α → α → Bool
n : Nat
a b : α
l : List α
h : (a :: b :: l).length = n + 2
w : l' = ⟨a :: b :: l, h⟩.val.reverse
⊢ mergeSortTR₂.run' le ⟨a :: b :: l, h⟩ = l'.mergeSort le

Tactic:
cases h

Result:
case refl
α : Type u_1
l' : List α
le : α → α → Bool
a b : α
l : List α
w : l' = ⟨a :: b :: l, ⋯⟩.val.reverse
⊢ mergeSortTR₂.run' le ⟨a :: b :: l, ⋯⟩ = l'.mergeSort le

Proof state:
case refl.cons.nil
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x : α
w : [x] = ⟨a :: b :: l, ⋯⟩.val.reverse
w' : [x].length = l.length + 2
⊢ (⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse.mergeSort le).merge
      (⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).snd.val, ⋯⟩.val.mergeSort le) le =
    [x].mergeSort le

Tactic:
simp at w'

Result:
no goals

Proof state:
case refl.cons.cons.e_ys.e_xs.e_a
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = (a :: b :: l).reverse
w' : (x :: y :: l').length = l.length + 2
⊢ (l.length + 2 + 1) / 2 = (l'.length + 1 + 1 + 1) / 2

Tactic:
simp at w'

Result:
case refl.cons.cons.e_ys.e_xs.e_a
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = (a :: b :: l).reverse
w' : l'.length = l.length
⊢ (l.length + 2 + 1) / 2 = (l'.length + 1 + 1 + 1) / 2