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

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
⊢ (a :: b :: xs).mergeSort 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
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ (a :: b :: xs).mergeSort le = a :: b :: xs

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
⊢ (a :: b :: xs).mergeSort 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
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
this✝ : (splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.length < xs.length + 1 + 1
this : (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.length < xs.length + 1 + 1
⊢ (a :: b :: xs).mergeSort le = a :: b :: xs

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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:
rw [mergeSort_of_sorted (splitInTwo_fst_sorted ⟨a :: b :: xs, rfl⟩ h)]

Result:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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.merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le = a :: b :: xs

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

Tactic:
simp [splitInTwo_fst]

Result:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
⊢ min ((xs.length + 1 + 1 + 1) / 2) (xs.length + 1 + 1) < xs.length + 1 + 1

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

Tactic:
rw [mergeSort]

Result:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
⊢ 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
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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.merge (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val le = a :: b :: xs

Tactic:
rw [merge_of_le (splitInTwo_fst_le_splitInTwo_snd h)]

Result:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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 ++ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val = a :: b :: xs

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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
le : α → α → Bool
a : α
x✝ : Pairwise (fun a b => le a b = true) [a]
⊢ [a].mergeSort le = [a]

Tactic:
simp [mergeSort]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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 ++ (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val = a :: b :: xs

Tactic:
rw [splitInTwo_fst_append_splitInTwo_snd]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
x✝ : Pairwise (fun a b => le a b = true) []
⊢ [].mergeSort le = []

Tactic:
simp [mergeSort]

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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.merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le) le = a :: b :: xs

Tactic:
rw [mergeSort_of_sorted (splitInTwo_snd_sorted ⟨a :: b :: xs, rfl⟩ h)]

Result:
α : Type u_1
le : α → α → Bool
a b : α
xs : List α
h : Pairwise (fun a b => le a b = true) (a :: b :: xs)
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.merge (splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val le = a :: b :: xs