case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ destutter' R a [] <+ [a]

case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ destutter' R a (b :: l) <+ a :: b :: l
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ destutter' R a l <+ a :: l
induction' l with b l hl generalizing a
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ destutter' R a (b :: l) <+ a :: b :: l
rw [destutter']
case cons.inl
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l

case cons.inr
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
⊢ (if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
split_ifs
no goals
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ destutter' R a [] <+ [a]
simp
no goals
case cons.inl
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : R a b
⊢ a :: destutter' R b l <+ a :: b :: l
exact Sublist.cons₂ a (hl b)
no goals
case cons.inr
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), destutter' R a l <+ a :: l
a : α
h✝ : ¬R a b
⊢ destutter' R a l <+ a :: b :: l
exact (hl a).trans ((l.sublist_cons b).cons_cons a)