-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem mergeSort_perm : ∀ (l : List α) (le), mergeSort l le ~ l
  | [], _ => by simp [mergeSort]
  | [a], _ => by simp [mergeSort]
  | a :: b :: xs, le => by
    simp only [mergeSort]
    have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
⊢ (a :: b :: xs).mergeSort le ~ a :: b :: xs

Tactic:
simp only [mergeSort]

Result:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
⊢ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le ~
    a :: b :: xs

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
⊢ (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1

Tactic:
simp [splitInTwo_fst]

Result:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
⊢ min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) < xs.length + 1 + 1

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
⊢ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le ~
    a :: b :: xs

Tactic:
have : (splitInTwo ⟨a :: b :: xs, rfl⟩).1.1.length < xs.length + 1 + 1 := by simp [splitInTwo_fst]; omega

Result:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le ~
    a :: b :: xs

Proof state:
α : Type u_1
a : α
x✝ : α → α → Bool
⊢ [a].mergeSort x✝ ~ [a]

Tactic:
simp [mergeSort]

Result:
no goals

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1

Tactic:
simp [splitInTwo_snd]

Result:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2 < xs.length + 1 + 1

Proof state:
α : Type u_1
x✝ : α → α → Bool
⊢ [].mergeSort x✝ ~ []

Tactic:
simp [mergeSort]

Result:
no goals

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ xs.length + 1 + 1 - (xs.length + 1 + 1 + 1) / 2 < xs.length + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le ~
    a :: b :: xs

Tactic:
exact (merge_perm_append le).trans
  (((mergeSort_perm _ _).append (mergeSort_perm _ _)).trans
    (Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))

Result:
no goals

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
⊢ min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) < xs.length + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le ~
    a :: b :: xs

Tactic:
have : (splitInTwo ⟨a :: b :: xs, rfl⟩).2.1.length < xs.length + 1 + 1 := by simp [splitInTwo_snd]; omega

Result:
α : Type u_1
a b : α
xs : List α
le : α → α → Bool
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le ~
    a :: b :: xs