-- 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:
α : Type u_1
l' : List α
le : α → α → Bool
a : α
property✝ : [a].length = 1
w : l' = ⟨[a], property✝⟩.val.reverse
⊢ mergeSortTR₂.run' le ⟨[a], property✝⟩ = l'.mergeSort le

Tactic:
simp_all [mergeSortTR₂.run', mergeSort]

Result:
no goals

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, ⋯⟩.val.reverse
w' : (x :: y :: l').length = l.length + 2
⊢ ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse =
    (splitInTwo ⟨x :: y :: l', ⋯⟩).fst.val

Tactic:
dsimp at w

Result:
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
⊢ ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).fst.val.reverse, ⋯⟩.val.reverse =
    (splitInTwo ⟨x :: y :: l', ⋯⟩).fst.val

Proof state:
case refl.cons.cons.e_ys.e_xs
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = ⟨a :: b :: l, ⋯⟩.val.reverse
w' : (x :: y :: l').length = l.length + 2
⊢ ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).snd.val, ⋯⟩.val = (splitInTwo ⟨x :: y :: l', ⋯⟩).snd.val

Tactic:
dsimp at w

Result:
case refl.cons.cons.e_ys.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
⊢ ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).snd.val, ⋯⟩.val = (splitInTwo ⟨x :: y :: l', ⋯⟩).snd.val

Proof state:
case refl.cons.cons.e_ys.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 ((l.length + 2 + 1) / 2) (l.reverse ++ [b, a]) = drop ((l'.length + 1 + 1 + 1) / 2) (l.reverse ++ [b, a])

Tactic:
congr 1

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' : (x :: y :: l').length = l.length + 2
⊢ (l.length + 2 + 1) / 2 = (l'.length + 1 + 1 + 1) / 2

Proof state:
case refl.cons.cons.e_ys.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
⊢ (splitInTwo ⟨(a :: b :: l).reverse, ⋯⟩).snd.val = (splitInTwo ⟨(a :: b :: l).reverse, ⋯⟩).snd.val

Tactic:
simp only [reverse_cons, append_assoc, singleton_append, splitInTwo_snd, length_cons]

Result:
case refl.cons.cons.e_ys.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 ((l.length + 2 + 1) / 2) (l.reverse ++ [b, a]) = drop ((l'.length + 1 + 1 + 1) / 2) (l.reverse ++ [b, a])

Proof state:
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

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

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

Proof state:
case refl.cons.cons
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = ⟨a :: b :: l, ⋯⟩.val.reverse
w' : (x :: y :: l').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 :: y :: l').mergeSort le

Tactic:
rw [mergeSort]

Result:
case refl.cons.cons
α : Type u_1
le : α → α → Bool
a b : α
l : List α
x y : α
l' : List α
w : x :: y :: l' = ⟨a :: b :: l, ⋯⟩.val.reverse
w' : (x :: y :: l').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 =
    ((splitInTwo ⟨x :: y :: l', ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨x :: y :: l', ⋯⟩).snd.val.mergeSort le) le

Proof state:
case refl
α : Type u_1
l' : List α
le : α → α → Bool
a b : α
l : List α
w : l' = ⟨a :: b :: l, ⋯⟩.val.reverse
⊢ (⟨(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 =
    l'.mergeSort le

Tactic:
have w' := congrArg length w

Result:
case refl
α : Type u_1
l' : List α
le : α → α → Bool
a b : α
l : List α
w : l' = ⟨a :: b :: l, ⋯⟩.val.reverse
w' : l'.length = ⟨a :: b :: l, ⋯⟩.val.reverse.length
⊢ (⟨(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 =
    l'.mergeSort le

Proof state:
case refl.cons.cons.e_ys.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
⊢ ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).snd.val, ⋯⟩.val = (splitInTwo ⟨x :: y :: l', ⋯⟩).snd.val

Tactic:
simp only [w]

Result:
case refl.cons.cons.e_ys.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
⊢ (splitInTwo ⟨(a :: b :: l).reverse, ⋯⟩).snd.val = (splitInTwo ⟨(a :: b :: l).reverse, ⋯⟩).snd.val

Proof state:
case refl.nil
α : Type u_1
le : α → α → Bool
a b : α
l : List α
w : [] = ⟨a :: b :: l, ⋯⟩.val.reverse
w' : [].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 =
    [].mergeSort le

Tactic:
simp at w'

Result:
no goals

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

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

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