case hc
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ r a b

α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ Sorted r (b :: l)
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ insertionSort r (a :: b :: l) = a :: b :: l
rw [insertionSort, Sorted.insertionSort_eq, orderedInsert, if_pos]
no goals
case hc
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ r a b

α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : Sorted r (a :: b :: l)
⊢ Sorted r (b :: l)
exacts [rel_of_sorted_cons h _ (mem_cons_self _ _), h.tail]