-- 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.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 - ((a :: b :: l).length + 1) / 2) (a :: b :: l)

Tactic:
simp

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

Tactic:
omega

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
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

Tactic:
simp at 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 = 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 =
    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 =
    ((splitInTwo ⟨x :: y :: l', ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨x :: y :: l', ⋯⟩).snd.val.mergeSort le) le

Tactic:
congr 2

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, ⋯⟩.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

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

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

Tactic:
simp only [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).reverse, ⋯⟩).fst.val.reverse.reverse = (splitInTwo ⟨(a :: b :: l).reverse, ⋯⟩).fst.val

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

Tactic:
simp only [splitInTwo_fst, splitInTwo_snd, reverse_take, take_reverse]

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
⊢ (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

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

Tactic:
rw [← merge_eq_mergeTR]

Result:
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

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 (splitRevInTwo' ⟨a :: b :: l, ⋯⟩).snd)
      (mergeSortTR₂.run le (splitRevInTwo' ⟨a :: b :: l, ⋯⟩).fst) le =
    l'.mergeSort le

Tactic:
rw [splitRevInTwo'_fst, splitRevInTwo'_snd]

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 ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).fst.val.reverse, ⋯⟩)
      (mergeSortTR₂.run le ⟨(splitInTwo ⟨⟨a :: b :: l, ⋯⟩.val.reverse, ⋯⟩).snd.val, ⋯⟩) le =
    l'.mergeSort le

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

Tactic:
rw [w, length_reverse]

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 - ((a :: b :: l).length + 1) / 2) (a :: b :: l)