[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R b a
⊢ destutter' R b (a :: l) = b :: destutter' R a l
[PROOFSTEP]
rw [destutter', if_pos h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R b a
⊢ destutter' R b (a :: l) = destutter' R b l
[PROOFSTEP]
rw [destutter', if_neg h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter' R a [b] = if R a b then [a, b] else [a]
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : R a b
⊢ destutter' R a [b] = [a, b]
[PROOFSTEP]
simp! [h]
[GOAL]
case neg
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : ¬R a b
⊢ destutter' R a [b] = [a]
[PROOFSTEP]
simp! [h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ destutter' R a l <+ a :: l
[PROOFSTEP]
induction' l with b l hl generalizing a
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ destutter' R a [] <+ [a]
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rw [destutter']
[GOAL]
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : 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
[PROOFSTEP]
exact Sublist.cons₂ a (hl b)
[GOAL]
case neg
α : 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
[PROOFSTEP]
exact (hl a).trans ((l.sublist_cons b).cons_cons a)
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R a l
[PROOFSTEP]
induction' l with b l hl
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ a ∈ destutter' R a []
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
rw [destutter']
[GOAL]
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : 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
[PROOFSTEP]
simp
[GOAL]
case neg
α : 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
[PROOFSTEP]
assumption
[GOAL]
α : 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))
[PROOFSTEP]
rw [destutter']
[GOAL]
α : 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)
[PROOFSTEP]
split_ifs with hbc
[GOAL]
case pos
α : 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)
[PROOFSTEP]
rw [chain_cons]
[GOAL]
case pos
α : 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)
[PROOFSTEP]
exact ⟨h, destutter'_is_chain l hbc⟩
[GOAL]
case neg
α : 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)
[PROOFSTEP]
exact destutter'_is_chain l h
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
⊢ Chain' R (destutter' R a l)
[PROOFSTEP]
induction' l with b l hl generalizing a
[GOAL]
case nil
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝¹ b a✝ a : α
⊢ Chain' R (destutter' R a [])
[PROOFSTEP]
simp
[GOAL]
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))
[PROOFSTEP]
rw [destutter']
[GOAL]
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)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : 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)
[PROOFSTEP]
exact destutter'_is_chain R l h
[GOAL]
case neg
α : 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)
[PROOFSTEP]
exact hl a
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
h : Chain R a l
⊢ destutter' R a l = a :: l
[PROOFSTEP]
induction' l with b l hb generalizing a
[GOAL]
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]
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
obtain ⟨h, hc⟩ := chain_cons.mp h
[GOAL]
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
[PROOFSTEP]
rw [l.destutter'_cons_pos h, hb hc]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain R a l
[PROOFSTEP]
suffices Chain' R (a :: l) by assumption
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
this : Chain' R (a :: l)
⊢ Chain R a l
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (a :: l)
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a✝ b a : α
h : destutter' R a l = a :: l
⊢ Chain' R (destutter' R a l)
[PROOFSTEP]
exact l.destutter'_is_chain' R a
[GOAL]
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a b : α
⊢ destutter R [] = [] ↔ Chain' R []
[PROOFSTEP]
simp
