no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
⊢ merge r [] [] ~ [] ++ []
simp [merge]
no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
b : α
l' : List α
⊢ merge r [] (b :: l') ~ [] ++ b :: l'
simp [merge]
no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
⊢ merge r (a :: l) [] ~ a :: l ++ []
simp [merge]
case pos
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : r a b
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'

case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
by_cases h : a ≼ b
no goals
case pos
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : r a b
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
simpa [merge, h] using perm_merge _ _
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
⊢ b :: merge r (a :: l) l' ~ a :: (l ++ b :: l')
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
suffices b :: merge r (a :: l) l' ~ a :: (l ++ b :: l') by simpa [merge, h]
no goals
case neg
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
⊢ b :: merge r (a :: l) l' ~ a :: (l ++ b :: l')
exact ((perm_merge _ _).cons _).trans ((swap _ _ _).trans (perm_middle.symm.cons _))
no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
b : α
l' : List α
h : ¬r a b
this : b :: merge r (a :: l) l' ~ a :: (l ++ b :: l')
⊢ merge r (a :: l) (b :: l') ~ a :: l ++ b :: l'
simpa [merge, h]