no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
⊢ mergeSort r [] ~ []
simp [mergeSort]
no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
⊢ mergeSort r [a] ~ [a]
simp [mergeSort]
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
cases' e : split (a :: b :: l) with l₁ l₂
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
case mk
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
cases' length_split_lt e with h₁ h₂
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ merge r (mergeSort r l₁) (mergeSort r l₂) ~ a :: b :: l
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ mergeSort r (a :: b :: l) ~ a :: b :: l
rw [mergeSort_cons_cons r e]
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ mergeSort r l₁ ++ mergeSort r l₂ ~ a :: b :: l
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ merge r (mergeSort r l₁) (mergeSort r l₂) ~ a :: b :: l
apply (perm_merge r _ _).trans
no goals
case mk.intro
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l l₁ l₂ : List α
e : split (a :: b :: l) = (l₁, l₂)
h₁ : length l₁ < length (a :: b :: l)
h₂ : length l₂ < length (a :: b :: l)
⊢ mergeSort r l₁ ++ mergeSort r l₂ ~ a :: b :: l
exact
  ((perm_mergeSort l₁).append (perm_mergeSort l₂)).trans (perm_split e).symm