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

case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (destutter' R a (b :: l))
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ Chain' R (destutter' R 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 : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (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 : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (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 : α), Chain' R (destutter' R a l)
a : α
h : R a b
⊢ Chain' R (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 : α), Chain' R (destutter' R a l)
a : α
h : ¬R a b
⊢ Chain' R (destutter' R a l)
case cons
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
⊢ Chain' R (if R a b then a :: destutter' R b l else destutter' R a l)
split_ifs with h
no goals
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ Chain' R (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 : α), Chain' R (destutter' R a l)
a : α
h : R a b
⊢ Chain' R (a :: destutter' R b l)
exact destutter'_is_chain R l h
no goals
case cons.inr
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b✝ a✝ b : α
l : List α
hl : ∀ (a : α), Chain' R (destutter' R a l)
a : α
h : ¬R a b
⊢ Chain' R (destutter' R a l)
exact hl a