case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R 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 ∈ destutter' R a (b :: l)
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R a l
induction' l with b l hl
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 ∈ if R a b then a :: destutter' R b l else destutter' R a 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 ∈ destutter' R 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
h✝ : R a b
⊢ a ∈ a :: destutter' R 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
h✝ : ¬R a b
⊢ a ∈ destutter' R a 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 ∈ if R a b then a :: destutter' R b l else destutter' R a l
split_ifs
no goals
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R 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
h✝ : R a b
⊢ a ∈ a :: destutter' R b l
simp
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
h✝ : ¬R a b
⊢ a ∈ destutter' R a l
assumption