-- 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 }) → mergeSortTR₂.run le l = mergeSort l.1 le
  | 0, ⟨[], _⟩
  | 1, ⟨[a], _⟩ => by simp [mergeSortTR₂.run, mergeSort]
  | n+2, ⟨a :: b :: l, h⟩ => by
    cases h
    simp only [mergeSortTR₂.run, mergeSort]
    rw [splitRevInTwo_fst, splitRevInTwo_snd]
    rw [mergeSortTR₂_run_eq_mergeSort, mergeSortTR₂_run'_eq_mergeSort]
    rw [merge_eq_mergeTR]
    rw [reverse_reverse]
termination_by n => n

Proof state:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSort ?m.68695 le) (⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val, ⋯⟩.val.mergeSort le) le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

case refl.w
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ ?m.68695 = ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse

α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ List α

Tactic:
rw [merge_eq_mergeTR]

Result:
case refl.w
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ (splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val = ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse

Proof state:
case refl.w
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ (splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val = ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse

Tactic:
rw [reverse_reverse]

Result:
no goals

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

Tactic:
simp only [mergeSortTR₂.run, mergeSort]

Result:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR₂.run' le (splitRevInTwo ⟨a :: b :: l, ⋯⟩).fst)
      (mergeSortTR₂.run le (splitRevInTwo ⟨a :: b :: l, ⋯⟩).snd) le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Proof state:
α : Type u_1
le : α → α → Bool
a : α
property✝ : [a].length = 1
⊢ mergeSortTR₂.run le ⟨[a], property✝⟩ = ⟨[a], property✝⟩.val.mergeSort le

Tactic:
simp [mergeSortTR₂.run, mergeSort]

Result:
no goals

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

Tactic:
cases h

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

Proof state:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR₂.run' le (splitRevInTwo ⟨a :: b :: l, ⋯⟩).fst)
      (mergeSortTR₂.run le (splitRevInTwo ⟨a :: b :: l, ⋯⟩).snd) le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Tactic:
rw [splitRevInTwo_fst, splitRevInTwo_snd]

Result:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR₂.run' le ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.reverse, ⋯⟩)
      (mergeSortTR₂.run le ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val, ⋯⟩) le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Proof state:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSortTR₂.run' le ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.reverse, ⋯⟩)
      (mergeSortTR₂.run le ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val, ⋯⟩) le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

Tactic:
rw [mergeSortTR₂_run_eq_mergeSort, mergeSortTR₂_run'_eq_mergeSort]

Result:
case refl
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ mergeTR (mergeSort ?m.68695 le) (⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val, ⋯⟩.val.mergeSort le) le =
    ((splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: l, ⋯⟩).snd.val.mergeSort le) le

case refl.w
α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ ?m.68695 = ⟨(splitInTwo ⟨a :: b :: l, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse

α : Type u_1
le : α → α → Bool
a b : α
l : List α
⊢ List α