α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (if R b c then b :: destutter' R c l else destutter' R b l)
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (destutter' R b (c :: l))
rw [destutter']
case inl
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ Chain R a (b :: destutter' R c l)

case inr
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : ¬R b c
⊢ Chain R a (destutter' R b l)
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
⊢ Chain R a (if R b c then b :: destutter' R c l else destutter' R b l)
split_ifs with hbc
case inl
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ R a b ∧ Chain R b (destutter' R c l)
case inl
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ Chain R a (b :: destutter' R c l)
rw [chain_cons]
no goals
case inl
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : R b c
⊢ R a b ∧ Chain R b (destutter' R c l)
exact ⟨h, destutter'_is_chain l hbc⟩
no goals
case inr
α : Type u_1
l✝ : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b✝ c : α
l : List α
a b : α
h : R a b
hbc : ¬R b c
⊢ Chain R a (destutter' R b l)
exact destutter'_is_chain l h