Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Eric Rodriguez, Eric Wieser

! This file was ported from Lean 3 source module data.list.destutter
! leanprover-community/mathlib commit 7b78d1776212a91ecc94cf601f83bdcc46b04213
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.List.Chain

/-!
# Destuttering of Lists

This file proves theorems about `List.destutter` (in `Data.List.Defs`), which greedily removes all
non-related items that are adjacent in a list, e.g. `[2, 2, 3, 3, 2].destutter (≠) = [2, 3, 2]`.
Note that we make no guarantees of being the longest sublist with this property; e.g.,
`[123, 1, 2, 5, 543, 1000].destutter (<) = [123, 543, 1000]`, but a longer ascending chain could be
`[1, 2, 5, 543, 1000]`.

## Main statements

* `List.destutter_sublist`: `l.destutter` is a sublist of `l`.
* `List.destutter_is_chain'`: `l.destutter` satisfies `Chain' R`.
* Analogies of these theorems for `List.destutter'`, which is the `destutter` equivalent of `Chain`.

## Tags

adjacent, chain, duplicates, remove, list, stutter, destutter
-/

variable {α: Type ?u.11569α : Type _: Type (?u.9441+1)Type _} (l: List αl : List: Type ?u.9444 → Type ?u.9444List α: Type ?u.160α) (R: α → α → PropR : α: Type ?u.1592α → α: Type ?u.2α → Prop: TypeProp) [DecidableRel: {α : Sort ?u.1604} → (α → α → Prop) → Sort (max1?u.1604)DecidableRel R: α → α → PropR] {a: αa b: αb : α: Type ?u.2α}

namespace List

@[simp]
theorem destutter'_nil: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter' R a [] = [a]destutter'_nil : destutter': {α : Type ?u.67} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa []: List ?m.77[] = [a: αa] :=
rfl: ∀ {α : Sort ?u.109} {a : α}, a = arfl
#align list.destutter'_nil List.destutter'_nil: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter' R a [] = [a]List.destutter'_nil

theorem destutter'_cons: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter' R a (b :: l) = if R a b then a :: destutter' R b l else destutter' R a ldestutter'_cons :
(b: αb :: l: List αl).destutter': {α : Type ?u.196} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa = if R: α → α → PropR a: αa b: αb then a: αa :: destutter': {α : Type ?u.242} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR b: αb l: List αl else destutter': {α : Type ?u.253} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa l: List αl :=
rfl: ∀ {α : Sort ?u.272} {a : α}, a = arfl
#align list.destutter'_cons List.destutter'_cons: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter' R a (b :: l) = if R a b then a :: destutter' R b l else destutter' R a lList.destutter'_cons

variable {R: ?m.369R}

@[simp]
theorem destutter'_cons_pos: ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
R b a → destutter' R b (a :: l) = b :: destutter' R a ldestutter'_cons_pos (h: R b ah : R: α → α → PropR b: αb a: αa) : (a: αa :: l: List αl).destutter': {α : Type ?u.410} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR b: αb = b: αb :: l: List αl.destutter': {α : Type ?u.452} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R b adestutter' R b (a :: l) = b :: destutter' R a lrw [α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R b adestutter' R b (a :: l) = b :: destutter' R a ldestutter': {α : Type ?u.1292} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter',α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R b a(if R b a then b :: destutter' R a l else destutter' R b l) = b :: destutter' R a l α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R b adestutter' R b (a :: l) = b :: destutter' R a lif_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1293} {t e : α}, (if c then t else e) = tif_pos h: R b ahα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R b ab :: destutter' R a l = b :: destutter' R a l]Goals accomplished! 🐙
#align list.destutter'_cons_pos List.destutter'_cons_pos: ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
R b a → destutter' R b (a :: l) = b :: destutter' R a lList.destutter'_cons_pos

@[simp]
theorem destutter'_cons_neg: ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
¬R b a → destutter' R b (a :: l) = destutter' R b ldestutter'_cons_neg (h: ¬R b ah : ¬R: α → α → PropR b: αb a: αa) : (a: αa :: l: List αl).destutter': {α : Type ?u.1400} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR b: αb = l: List αl.destutter': {α : Type ?u.1440} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR b: αb := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R b adestutter' R b (a :: l) = destutter' R b lrw [α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R b adestutter' R b (a :: l) = destutter' R b ldestutter': {α : Type ?u.1518} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter',α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R b a(if R b a then b :: destutter' R a l else destutter' R b l) = destutter' R b l α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R b adestutter' R b (a :: l) = destutter' R b lif_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1519} {t e : α}, (if c then t else e) = eif_neg h: ¬R b ahα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R b adestutter' R b l = destutter' R b l]Goals accomplished! 🐙
#align list.destutter'_cons_neg List.destutter'_cons_neg: ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
¬R b a → destutter' R b (a :: l) = destutter' R b lList.destutter'_cons_neg

variable (R: ?m.1624R)

@[simp]
theorem destutter'_singleton: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter' R a [b] = if R a b then [a, b] else [a]destutter'_singleton : [b: αb].destutter': {α : Type ?u.1665} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa = if R: α → α → PropR a: αa b: αb then [a: αa, b: αb] else [a: αa] := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αdestutter' R a [b] = if R a b then [a, b] else [a]split_ifs with hα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R a binldestutter' R a [b] = [a, b]α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R a binrdestutter' R a [b] = [a] α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αdestutter' R a [b] = if R a b then [a, b] else [a]<;>α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: R a binldestutter' R a [b] = [a, b]α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: ¬R a binrdestutter' R a [b] = [a] α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αdestutter' R a [b] = if R a b then [a, b] else [a]simp! [h: ¬R a bh]Goals accomplished! 🐙
#align list.destutter'_singleton List.destutter'_singleton: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter' R a [b] = if R a b then [a, b] else [a]List.destutter'_singleton

theorem destutter'_sublist: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), destutter' R a l <+ a :: ldestutter'_sublist (a: ?m.3014a) : l: List αl.destutter': {α : Type ?u.3019} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: ?m.3014a <+ a: ?m.3014a :: l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αdestutter' R a l <+ a :: linduction' l: List αl with b: ?m.3086b l: List ?m.3086l hl: ?m.3087 lhl generalizing a: αaα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b, a✝, a: αnildestutter' R a [] <+ [a]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αconsdestutter' R a (b :: l) <+ a :: b :: l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αdestutter' R a l <+ a :: l·α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b, a✝, a: αnildestutter' R a [] <+ [a] α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b, a✝, a: αnildestutter' R a [] <+ [a]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αconsdestutter' R a (b :: l) <+ a :: b :: lsimpGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αdestutter' R a l <+ a :: lrw [α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αconsdestutter' R a (b :: l) <+ a :: b :: ldestutter': {α : Type ?u.3358} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter'α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αcons(if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αcons(if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αdestutter' R a l <+ a :: lsplit_ifsα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: R a bcons.inla :: destutter' R b l <+ a :: b :: lα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: ¬R a bcons.inrdestutter' R a l <+ a :: b :: l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αdestutter' R a l <+ a :: l·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: R a bcons.inla :: destutter' R b l <+ a :: b :: l α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: R a bcons.inla :: destutter' R b l <+ a :: b :: lα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: ¬R a bcons.inrdestutter' R a l <+ a :: b :: lexact Sublist.cons₂: ∀ {α : Type ?u.3865} {l₁ l₂ : List α} (a : α), l₁ <+ l₂ → a :: l₁ <+ a :: l₂Sublist.cons₂ a: αa (hl: ?m.3087 lhl b: ?m.3086b)Goals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αdestutter' R a l <+ a :: l·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: ¬R a bcons.inrdestutter' R a l <+ a :: b :: l α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), destutter' R a l <+ a :: la: αh✝: ¬R a bcons.inrdestutter' R a l <+ a :: b :: lexact (hl: ?m.3087 lhl a: αa).trans: ∀ {α : Type ?u.3875} {l₁ l₂ l₃ : List α}, l₁ <+ l₂ → l₂ <+ l₃ → l₁ <+ l₃trans ((l: List ?m.3086l.sublist_cons: ∀ {α : Type ?u.3886} (a : α) (l : List α), l <+ a :: lsublist_cons b: ?m.3086b).cons_cons: ∀ {α : Type ?u.3891} {l₁ l₂ : List α} (a : α), l₁ <+ l₂ → a :: l₁ <+ a :: l₂cons_cons a: αa)Goals accomplished! 🐙
#align list.destutter'_sublist List.destutter'_sublist: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), destutter' R a l <+ a :: lList.destutter'_sublist

theorem mem_destutter': ∀ (a : α), a ∈ destutter' R a lmem_destutter' (a: αa) : a: ?m.3958a ∈ l: List αl.destutter': {α : Type ?u.3976} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: ?m.3958a := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αa ∈ destutter' R a linduction' l: List αl with b: ?m.4049b l: List ?m.4049l hl: ?m.4050 lhlα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αnila ∈ destutter' R a []α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lconsa ∈ destutter' R a (b :: l)
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αa ∈ destutter' R a l·α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αnila ∈ destutter' R a [] α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αnila ∈ destutter' R a []α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lconsa ∈ destutter' R a (b :: l)simpGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αa ∈ destutter' R a lrw [α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lconsa ∈ destutter' R a (b :: l)destutter': {α : Type ?u.4342} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter'α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lconsa ∈ if R a b then a :: destutter' R b l else destutter' R a l]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lconsa ∈ if R a b then a :: destutter' R b l else destutter' R a l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αa ∈ destutter' R a lsplit_ifsα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: R a bcons.inla ∈ a :: destutter' R b lα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: ¬R a bcons.inra ∈ destutter' R a l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αa ∈ destutter' R a l·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: R a bcons.inla ∈ a :: destutter' R b l α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: R a bcons.inla ∈ a :: destutter' R b lα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: ¬R a bcons.inra ∈ destutter' R a lsimpGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αa ∈ destutter' R a l·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: ¬R a bcons.inra ∈ destutter' R a l α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, a, b: αl: List αhl: a ∈ destutter' R a lh✝: ¬R a bcons.inra ∈ destutter' R a lassumptionGoals accomplished! 🐙
#align list.mem_destutter' List.mem_destutter': ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), a ∈ destutter' R a lList.mem_destutter'

theorem destutter'_is_chain: ∀ (l : List α) {a b : α}, R a b → Chain R a (destutter' R b l)destutter'_is_chain : ∀ l: List αl : List: Type ?u.8293 → Type ?u.8293List α: Type ?u.8260α, ∀ {a: ?m.8297a b: ?m.8300b}, R: α → α → PropR a: ?m.8297a b: ?m.8300b → (l: List αl.destutter': {α : Type ?u.8305} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR b: ?m.8300b).Chain: {α : Type ?u.8346} → (α → α → Prop) → α → List α → PropChain R: α → α → PropR a: ?m.8297a
| [], a: αa, b: αb, h: R a bh => chain_singleton: ∀ {α : Type ?u.8411} {R : α → α → Prop} {a b : α}, Chain R a [b] ↔ R a bchain_singleton.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr h: R a bh
| c: αc :: l: List αl, a: αa, b: αb, h: R a bh => byGoals accomplished! 🐙
α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (destutter' R b (c :: l))rw [α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (destutter' R b (c :: l))destutter': {α : Type ?u.8707} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter'α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (if R b c then b :: destutter' R c l else destutter' R b l)]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (if R b c then b :: destutter' R c l else destutter' R b l)
α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (destutter' R b (c :: l))split_ifs with hbcα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlChain R a (b :: destutter' R c l)α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: ¬R b cinrChain R a (destutter' R b l)
α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (destutter' R b (c :: l))·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlChain R a (b :: destutter' R c l) α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlChain R a (b :: destutter' R c l)α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: ¬R b cinrChain R a (destutter' R b l)rw [α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlChain R a (b :: destutter' R c l)chain_cons: ∀ {α : Type ?u.9237} {R : α → α → Prop} {a b : α} {l : List α}, Chain R a (b :: l) ↔ R a b ∧ Chain R b lchain_consα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlR a b ∧ Chain R b (destutter' R c l)]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlR a b ∧ Chain R b (destutter' R c l)
α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: R b cinlChain R a (b :: destutter' R c l)exact ⟨h: R a bh, destutter'_is_chain: ∀ (l : List α) {a b : α}, R a b → Chain R a (destutter' R b l)destutter'_is_chain l: List αl hbc: R b chbc⟩Goals accomplished! 🐙
α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bChain R a (destutter' R b (c :: l))·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: ¬R b cinrChain R a (destutter' R b l) α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝, c: αl: List αa, b: αh: R a bhbc: ¬R b cinrChain R a (destutter' R b l)exact destutter'_is_chain: ∀ (l : List α) {a b : α}, R a b → Chain R a (destutter' R b l)destutter'_is_chain l: List αl h: R a bhGoals accomplished! 🐙
#align list.destutter'_is_chain List.destutter'_is_chain: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α) {a b : α}, R a b → Chain R a (destutter' R b l)List.destutter'_is_chain

theorem destutter'_is_chain': ∀ (a : α), Chain' R (destutter' R a l)destutter'_is_chain' (a: αa) : (l: List αl.destutter': {α : Type ?u.9476} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: ?m.9473a).Chain': {α : Type ?u.9517} → (α → α → Prop) → List α → PropChain' R: α → α → PropR := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αChain' R (destutter' R a l)induction' l: List αl with b: ?m.9552b l: List ?m.9552l hl: ?m.9553 lhl generalizing a: αaα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b, a✝, a: αnilChain' R (destutter' R a [])α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αconsChain' R (destutter' R a (b :: l))
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αChain' R (destutter' R a l)·α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b, a✝, a: αnilChain' R (destutter' R a []) α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b, a✝, a: αnilChain' R (destutter' R a [])α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αconsChain' R (destutter' R a (b :: l))simpGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αChain' R (destutter' R a l)rw [α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αconsChain' R (destutter' R a (b :: l))destutter': {α : Type ?u.9835} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter'α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αconsChain' R (if R a b then a :: destutter' R b l else destutter' R a l)]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αconsChain' R (if R a b then a :: destutter' R b l else destutter' R a l)
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αChain' R (destutter' R a l)split_ifs with hα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: R a bcons.inlChain' R (a :: destutter' R b l)α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: ¬R a bcons.inrChain' R (destutter' R a l)
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αChain' R (destutter' R a l)·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: R a bcons.inlChain' R (a :: destutter' R b l) α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: R a bcons.inlChain' R (a :: destutter' R b l)α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: ¬R a bcons.inrChain' R (destutter' R a l)exact destutter'_is_chain: ∀ {α : Type ?u.10339} (R : α → α → Prop) [inst : DecidableRel R] (l : List α) {a b : α},
R a b → Chain R a (destutter' R b l)destutter'_is_chain R: α → α → PropR l: List ?m.9552l h: R a bhGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αChain' R (destutter' R a l)·α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: ¬R a bcons.inrChain' R (destutter' R a l) α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝¹, b✝, a✝, b: αl: List αhl: ∀ (a : α), Chain' R (destutter' R a l)a: αh: ¬R a bcons.inrChain' R (destutter' R a l)exact hl: ?m.9553 lhl a: αaGoals accomplished! 🐙
#align list.destutter'_is_chain' List.destutter'_is_chain': ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), Chain' R (destutter' R a l)List.destutter'_is_chain'

theorem destutter'_of_chain: Chain R a l → destutter' R a l = a :: ldestutter'_of_chain (h: Chain R a lh : l: List αl.Chain: {α : Type ?u.10450} → (α → α → Prop) → α → List α → PropChain R: α → α → PropR a: αa) : l: List αl.destutter': {α : Type ?u.10466} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa = a: αa :: l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: Chain R a ldestutter' R a l = a :: linduction' l: List αl with b: ?m.10533b l: List ?m.10533l hb: ?m.10534 lhb generalizing a: αaα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b: αh✝: Chain R a✝ la: αh: Chain R a []nildestutter' R a [] = [a]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh: Chain R a (b :: l)consdestutter' R a (b :: l) = a :: b :: l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: Chain R a ldestutter' R a l = a :: l·α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b: αh✝: Chain R a✝ la: αh: Chain R a []nildestutter' R a [] = [a] α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b: αh✝: Chain R a✝ la: αh: Chain R a []nildestutter' R a [] = [a]α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh: Chain R a (b :: l)consdestutter' R a (b :: l) = a :: b :: lsimpGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: Chain R a ldestutter' R a l = a :: lobtain ⟨h, hc⟩: R a b ∧ Chain R b l⟨h: R a bh⟨h, hc⟩: R a b ∧ Chain R b l, hc: Chain R b lhc⟨h, hc⟩: R a b ∧ Chain R b l⟩ := chain_cons: ∀ {α : Type ?u.10759} {R : α → α → Prop} {a b : α} {l : List α}, Chain R a (b :: l) ↔ R a b ∧ Chain R b lchain_cons.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp h: Chain R a (b :: l)hα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝¹: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh✝: Chain R a (b :: l)h: R a bhc: Chain R b lcons.introdestutter' R a (b :: l) = a :: b :: l
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αh: Chain R a ldestutter' R a l = a :: lrw [α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝¹: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh✝: Chain R a (b :: l)h: R a bhc: Chain R b lcons.introdestutter' R a (b :: l) = a :: b :: ll: List ?m.10533l.destutter'_cons_pos: ∀ {α : Type ?u.10810} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
R b a → destutter' R b (a :: l) = b :: destutter' R a ldestutter'_cons_pos h: R a bh,α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝¹: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh✝: Chain R a (b :: l)h: R a bhc: Chain R b lcons.introa :: destutter' R b l = a :: b :: l α: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝¹: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh✝: Chain R a (b :: l)h: R a bhc: Chain R b lcons.introdestutter' R a (b :: l) = a :: b :: lhb: ?m.10534 lhb hc: Chain R b lhcα: Type u_1l✝: List αR: α → α → Propinst✝: DecidableRel Ra✝, b✝: αh✝¹: Chain R a✝ l✝b: αl: List αhb: ∀ {a : α}, Chain R a l → destutter' R a l = a :: la: αh✝: Chain R a (b :: l)h: R a bhc: Chain R b lcons.introa :: b :: l = a :: b :: l]Goals accomplished! 🐙
#align list.destutter'_of_chain List.destutter'_of_chain: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
Chain R a l → destutter' R a l = a :: lList.destutter'_of_chain

@[simp]
theorem destutter'_eq_self_iff: ∀ (a : α), destutter' R a l = a :: l ↔ Chain R a ldestutter'_eq_self_iff (a: ?m.10912a) : l: List αl.destutter': {α : Type ?u.10916} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: ?m.10912a = a: ?m.10912a :: l: List αl ↔ l: List αl.Chain: {α : Type ?u.10960} → (α → α → Prop) → α → List α → PropChain R: α → α → PropR a: ?m.10912a :=
⟨fun h: ?m.10983h => byGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain R a lsuffices Chain': {α : Type ?u.11138} → (α → α → Prop) → List α → PropChain' R: α → α → PropR (a: αa::l: List αl) by
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain R a lassumptionGoals accomplished! 🐙
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain R a lrw [α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain' R (a :: l)← h: destutter' R a l = a :: lhα: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain' R (destutter' R a l)]α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain' R (destutter' R a l)
α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra✝, b, a: αh: destutter' R a l = a :: lChain R a lexact l: List αl.destutter'_is_chain': ∀ {α : Type ?u.11179} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), Chain' R (destutter' R a l)destutter'_is_chain' R: α → α → PropR a: αaGoals accomplished! 🐙, destutter'_of_chain: ∀ {α : Type ?u.10989} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
Chain R a l → destutter' R a l = a :: ldestutter'_of_chain _: List ?m.10990_ _: ?m.10990 → ?m.10990 → Prop_⟩
#align list.destutter'_eq_self_iff List.destutter'_eq_self_iff: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α),
destutter' R a l = a :: l ↔ Chain R a lList.destutter'_eq_self_iff

theorem destutter'_ne_nil: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter' R a l ≠ []destutter'_ne_nil : l: List αl.destutter': {α : Type ?u.11324} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa ≠ []: List ?m.11366[] :=
ne_nil_of_mem: ∀ {α : Type ?u.11368} {a : α} {l : List α}, a ∈ l → l ≠ []ne_nil_of_mem <| l: List αl.mem_destutter': ∀ {α : Type ?u.11379} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), a ∈ destutter' R a lmem_destutter' R: α → α → PropR a: αa
#align list.destutter'_ne_nil List.destutter'_ne_nil: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter' R a l ≠ []List.destutter'_ne_nil

@[simp]
theorem destutter_nil: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R], destutter R [] = []destutter_nil : ([]: List ?m.11451[] : List: Type ?u.11449 → Type ?u.11449List α: Type ?u.11415α).destutter: {α : Type ?u.11453} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR = []: List ?m.11493[] :=
rfl: ∀ {α : Sort ?u.11523} {a : α}, a = arfl
#align list.destutter_nil List.destutter_nil: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R], destutter R [] = []List.destutter_nil

theorem destutter_cons': destutter R (a :: l) = destutter' R a ldestutter_cons' : (a: αa :: l: List αl).destutter: {α : Type ?u.11605} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR = destutter': {α : Type ?u.11644} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa l: List αl :=
rfl: ∀ {α : Sort ?u.11657} {a : α}, a = arfl
#align list.destutter_cons' List.destutter_cons': ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
destutter R (a :: l) = destutter' R a lList.destutter_cons'

theorem destutter_cons_cons: destutter R (a :: b :: l) = if R a b then a :: destutter' R b l else destutter' R a ldestutter_cons_cons :
(a: αa :: b: αb :: l: List αl).destutter: {α : Type ?u.11753} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR = if R: α → α → PropR a: αa b: αb then a: αa :: destutter': {α : Type ?u.11798} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR b: αb l: List αl else destutter': {α : Type ?u.11809} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List αdestutter' R: α → α → PropR a: αa l: List αl :=
rfl: ∀ {α : Sort ?u.11828} {a : α}, a = arfl
#align list.destutter_cons_cons List.destutter_cons_cons: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter R (a :: b :: l) = if R a b then a :: destutter' R b l else destutter' R a lList.destutter_cons_cons

@[simp]
theorem destutter_singleton: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter R [a] = [a]destutter_singleton : destutter: {α : Type ?u.11937} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR [a: αa] = [a: αa] :=
rfl: ∀ {α : Sort ?u.11981} {a : α}, a = arfl
#align list.destutter_singleton List.destutter_singleton: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter R [a] = [a]List.destutter_singleton

@[simp]
theorem destutter_pair: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter R [a, b] = if R a b then [a, b] else [a]destutter_pair : destutter: {α : Type ?u.12076} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR [a: αa, b: αb] = if R: α → α → PropR a: αa b: αb then [a: αa, b: αb] else [a: αa] :=
destutter_cons_cons: ∀ {α : Type ?u.12138} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter R (a :: b :: l) = if R a b then a :: destutter' R b l else destutter' R a ldestutter_cons_cons _: List ?m.12139_ R: α → α → PropR
#align list.destutter_pair List.destutter_pair: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
destutter R [a, b] = if R a b then [a, b] else [a]List.destutter_pair

theorem destutter_sublist: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), destutter R l <+ ldestutter_sublist : ∀ l: List αl : List: Type ?u.12263 → Type ?u.12263List α: Type ?u.12230α, l: List αl.destutter: {α : Type ?u.12268} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR <+ l: List αl
| [] => Sublist.slnil: ∀ {α : Type ?u.12326}, [] <+ []Sublist.slnil
| h: αh :: l: List αl => l: List αl.destutter'_sublist: ∀ {α : Type ?u.12363} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), destutter' R a l <+ a :: ldestutter'_sublist R: α → α → PropR h: αh
#align list.destutter_sublist List.destutter_sublist: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), destutter R l <+ lList.destutter_sublist

theorem destutter_is_chain': ∀ (l : List α), Chain' R (destutter R l)destutter_is_chain' : ∀ l: List αl : List: Type ?u.12531 → Type ?u.12531List α: Type ?u.12498α, (l: List αl.destutter: {α : Type ?u.12534} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR).Chain': {α : Type ?u.12574} → (α → α → Prop) → List α → PropChain' R: α → α → PropR
| [] => List.chain'_nil: ∀ {α : Type ?u.12625} {R : α → α → Prop}, Chain' R []List.chain'_nil
| h: αh :: l: List αl => l: List αl.destutter'_is_chain': ∀ {α : Type ?u.12686} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), Chain' R (destutter' R a l)destutter'_is_chain' R: α → α → PropR h: αh
#align list.destutter_is_chain' List.destutter_is_chain': ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), Chain' R (destutter R l)List.destutter_is_chain'

theorem destutter_of_chain': ∀ (l : List α), Chain' R l → destutter R l = ldestutter_of_chain' : ∀ l: List αl : List: Type ?u.12869 → Type ?u.12869List α: Type ?u.12836α, l: List αl.Chain': {α : Type ?u.12873} → (α → α → Prop) → List α → PropChain' R: α → α → PropR → l: List αl.destutter: {α : Type ?u.12887} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR = l: List αl
| [], _ => rfl: ∀ {α : Sort ?u.12968} {a : α}, a = arfl
| _ :: l: List αl, h: Chain' R (head✝ :: l)h => l: List αl.destutter'_of_chain: ∀ {α : Type ?u.13020} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
Chain R a l → destutter' R a l = a :: ldestutter'_of_chain _: ?m.13029 → ?m.13029 → Prop_ h: Chain' R (head✝ :: l)h
#align list.destutter_of_chain' List.destutter_of_chain': ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), Chain' R l → destutter R l = lList.destutter_of_chain'

@[simp]
theorem destutter_eq_self_iff: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), destutter R l = l ↔ Chain' R ldestutter_eq_self_iff : ∀ l: List αl : List: Type ?u.13355 → Type ?u.13355List α: Type ?u.13322α, l: List αl.destutter: {α : Type ?u.13359} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR = l: List αl ↔ l: List αl.Chain': {α : Type ?u.13400} → (α → α → Prop) → List α → PropChain' R: α → α → PropR
| [] => byGoals accomplished! 🐙 α: Type u_1l: List αR: α → α → Propinst✝: DecidableRel Ra, b: αdestutter R [] = [] ↔ Chain' R []simpGoals accomplished! 🐙
| a: αa :: l: List αl => l: List αl.destutter'_eq_self_iff: ∀ {α : Type ?u.13451} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α),
destutter' R a l = a :: l ↔ Chain R a ldestutter'_eq_self_iff R: α → α → PropR a: αa
#align list.destutter_eq_self_iff List.destutter_eq_self_iff: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), destutter R l = l ↔ Chain' R lList.destutter_eq_self_iff

theorem destutter_idem: destutter R (destutter R l) = destutter R ldestutter_idem : (l: List αl.destutter: {α : Type ?u.13873} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR).destutter: {α : Type ?u.13913} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR = l: List αl.destutter: {α : Type ?u.13930} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR :=
destutter_of_chain': ∀ {α : Type ?u.13949} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), Chain' R l → destutter R l = ldestutter_of_chain' R: α → α → PropR _: List ?m.13950_ <| l: List αl.destutter_is_chain': ∀ {α : Type ?u.13991} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), Chain' R (destutter R l)destutter_is_chain' R: α → α → PropR
#align list.destutter_idem List.destutter_idem: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R], destutter R (destutter R l) = destutter R lList.destutter_idem

@[simp]
theorem destutter_eq_nil: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {l : List α}, destutter R l = [] ↔ l = []destutter_eq_nil : ∀ {l: List αl : List: Type ?u.14085 → Type ?u.14085List α: Type ?u.14052α}, destutter: {α : Type ?u.14089} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List αdestutter R: α → α → PropR l: List αl = []: List ?m.14124[] ↔ l: List αl = []: List ?m.14155[]
| [] => Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl
| _ :: l: List αl => ⟨fun h: ?m.14244h => absurd: ∀ {a : Prop} {b : Sort ?u.14246}, a → ¬a → babsurd h: ?m.14244h <| l: List αl.destutter'_ne_nil: ∀ {α : Type ?u.14249} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α}, destutter' R a l ≠ []destutter'_ne_nil R: α → α → PropR, fun h: ?m.14307h => nomatch h: ?m.14307h⟩
#align list.destutter_eq_nil List.destutter_eq_nil: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] {l : List α}, destutter R l = [] ↔ l = []List.destutter_eq_nil

end List
```