-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem sorted_mergeSort
    (trans : ∀ (a b c : α), le a b → le b c → le a c)
    (total : ∀ (a b : α), le a b || le b a) :
    (l : List α) → (mergeSort l le).Pairwise le
  | [] => by simp [mergeSort]
  | [a] => by simp [mergeSort]
  | a :: b :: xs => by
    rw [mergeSort]
    apply sorted_merge @trans @total
    apply sorted_mergeSort trans total
    apply sorted_mergeSort trans total
termination_by l => l.length

Proof state:
case h₁
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le)

case h₂
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le)

Tactic:
apply sorted_mergeSort trans total

Result:
case h₂
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le)

Proof state:
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((a :: b :: xs).mergeSort le)

Tactic:
rw [mergeSort]

Result:
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true)
    (((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le)
      le)

Proof state:
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true)
    (((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le).merge ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le)
      le)

Tactic:
apply sorted_merge @trans @total

Result:
case h₁
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((splitInTwo ⟨a :: b :: xs, ⋯⟩).fst.val.mergeSort le)

case h₂
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le)

Proof state:
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
⊢ Pairwise (fun a b => le a b = true) ([].mergeSort le)

Tactic:
simp [mergeSort]

Result:
no goals

Proof state:
case h₂
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a b : α
xs : List α
⊢ Pairwise (fun a b => le a b = true) ((splitInTwo ⟨a :: b :: xs, ⋯⟩).snd.val.mergeSort le)

Tactic:
apply sorted_mergeSort trans total

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
trans : ∀ (a b c : α), le a b = true → le b c = true → le a c = true
total : ∀ (a b : α), (le a b || le b a) = true
a : α
⊢ Pairwise (fun a b => le a b = true) ([a].mergeSort le)

Tactic:
simp [mergeSort]

Result:
no goals