case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b : α
h✝ : Chain R a✝ l
a : α
h : Chain R a []
⊢ destutter' R a [] = [a]

case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ : α
h✝ : Chain R a✝ l✝
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h : Chain R a (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : Chain R a l
⊢ destutter' R a l = a :: l
induction' l with b l hb generalizing a
case cons.intro
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ : α
h✝¹ : Chain R a✝ l✝
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h✝ : Chain R a (b :: l)
h : R a b
hc : Chain R b l
⊢ destutter' R a (b :: l) = a :: b :: l
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ : α
h✝ : Chain R a✝ l✝
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h : Chain R a (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l
obtain ⟨h, hc⟩ := chain_cons.mp h
no goals
case cons.intro
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ : α
h✝¹ : Chain R a✝ l✝
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h✝ : Chain R a (b :: l)
h : R a b
hc : Chain R b l
⊢ destutter' R a (b :: l) = a :: b :: l
rw [l.destutter'_cons_pos h, hb hc]
no goals
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b : α
h✝ : Chain R a✝ l
a : α
h : Chain R a []
⊢ destutter' R a [] = [a]
simp