/-
Copyright (c) 2022 Eric Rodriguez. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.9444
List 
α: Type ?u.160
α) (
R: α → α → Prop
R : 
α: Type ?u.1592
α → 
α: Type ?u.2
α → 
Prop: Type
Prop) [
DecidableRel: {α : Sort ?u.1604} → (α → α → Prop) → Sort (max1?u.1604)
DecidableRel 
R: α → α → Prop
R] {
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: α → α → Prop
R 
a: α
a 
[]: List ?m.77
[] = [
a: α
a] :=
  
rfl: ∀ {α : Sort ?u.109} {a : α}, a = a
rfl
#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 l
destutter'_cons :
    (
b: α
b :: 
l: List α
l).
destutter': {α : Type ?u.196} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: α
a = if 
R: α → α → Prop
R 
a: α
a 
b: α
b then 
a: α
a :: 
destutter': {α : Type ?u.242} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
b: α
b 
l: List α
l else 
destutter': {α : Type ?u.253} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: α
a 
l: List α
l :=
  
rfl: ∀ {α : Sort ?u.272} {a : α}, a = a
rfl
#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 l
List.destutter'_cons

variable {
R: ?m.369
R}

@[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 l
destutter'_cons_pos (
h: R b a
h : 
R: α → α → Prop
R 
b: α
b 
a: α
a) : (
a: α
a :: 
l: List α
l).
destutter': {α : Type ?u.410} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
b: α
b = 
b: α
b :: 
l: List α
l.
destutter': {α : Type ?u.452} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: α
a := by
Goals accomplished! 🐙
  
α: 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 lrw [
α: 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
destutter': {α : Type ?u.1292} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter',
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, 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_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: R b a

destutter' R b (a :: l) = b :: destutter' R a l
if_pos: ∀ {c : Prop} {h : Decidable c}, c → ∀ {α : Sort ?u.1293} {t e : α}, (if c then t else e) = t
if_pos 
h: R b a
h
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: R b a

b :: 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 l
List.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 l
destutter'_cons_neg (
h: ¬R b a
h : ¬
R: α → α → Prop
R 
b: α
b 
a: α
a) : (
a: α
a :: 
l: List α
l).
destutter': {α : Type ?u.1400} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
b: α
b = 
l: List α
l.
destutter': {α : Type ?u.1440} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
b: α
b := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: ¬R b a

destutter' R b (a :: l) = destutter' R b lrw [
α: 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
destutter': {α : Type ?u.1518} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter',
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, 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_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: ¬R b a

destutter' R b (a :: l) = destutter' R b l
if_neg: ∀ {c : Prop} {h : Decidable c}, ¬c → ∀ {α : Sort ?u.1519} {t e : α}, (if c then t else e) = e
if_neg 
h: ¬R b a
h
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: ¬R b a

destutter' 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 l
List.destutter'_cons_neg

variable (
R: ?m.1624
R)

@[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: α → α → Prop
R 
a: α
a = if 
R: α → α → Prop
R 
a: α
a 
b: α
b then [
a: α
a, 
b: α
b] else [
a: α
a] := by
Goals accomplished! 🐙
  
α: 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]split_ifs with h
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: R a b

inl
destutter' R a [b] = [a, b]
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: ¬R a b

inr
destutter' R a [b] = [a] 
α: 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]<;>
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: R a b

inl
destutter' R a [b] = [a, b]
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: ¬R a b

inr
destutter' R a [b] = [a] 
α: 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]simp! [
h: ¬R a b
h]
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 :: l
destutter'_sublist (
a: ?m.3014
a) : 
l: List α
l.
destutter': {α : Type ?u.3019} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: ?m.3014
a <+ 
a: ?m.3014
a :: 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

destutter' R a l <+ a :: linduction' 
l: List α
l with 
b: ?m.3086
b 
l: List ?m.3086
l 
hl: ?m.3087 l
hl generalizing 
a: α
a
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝¹, b, a✝, a: α

nil
destutter' R a [] <+ [a]
α: 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: α

cons
destutter' R a (b :: l) <+ a :: b :: l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

destutter' R a l <+ a :: l·
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝¹, b, a✝, a: α

nil
destutter' R a [] <+ [a] 
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝¹, b, a✝, a: α

nil
destutter' R a [] <+ [a]
α: 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: α

cons
destutter' R a (b :: l) <+ a :: b :: lsimp
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

destutter' R a l <+ a :: lrw [
α: 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: α

cons
destutter' R a (b :: l) <+ a :: b :: l
destutter': {α : Type ?u.3358} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter'
α: 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: α

cons
(if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l]
α: 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: α

cons
(if R a b then a :: destutter' R b l else destutter' R a l) <+ a :: b :: l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

destutter' R a l <+ a :: lsplit_ifs
α: 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

cons.inl
a :: destutter' R b l <+ a :: b :: l
α: 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

cons.inr
destutter' R a l <+ a :: b :: l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

destutter' R a l <+ a :: l·
α: 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

cons.inl
a :: destutter' R b l <+ a :: b :: l 
α: 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

cons.inl
a :: destutter' R b l <+ a :: b :: l
α: 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

cons.inr
destutter' 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 l
hl 
b: ?m.3086
b)
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

destutter' R a l <+ a :: l·
α: 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

cons.inr
destutter' R a l <+ a :: b :: l 
α: 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

cons.inr
destutter' R a l <+ a :: b :: lexact (
hl: ?m.3087 l
hl 
a: α
a).
trans: ∀ {α : Type ?u.3875} {l₁ l₂ l₃ : List α}, l₁ <+ l₂ → l₂ <+ l₃ → l₁ <+ l₃
trans ((
l: List ?m.3086
l.
sublist_cons: ∀ {α : Type ?u.3886} (a : α) (l : List α), l <+ a :: l
sublist_cons 
b: ?m.3086
b).
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 :: l
List.destutter'_sublist

theorem 
mem_destutter': ∀ (a : α), a ∈ destutter' R a l
mem_destutter' (
a: α
a) : 
a: ?m.3958
a ∈ 
l: List α
l.
destutter': {α : Type ?u.3976} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: ?m.3958
a := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

a ∈ destutter' R a linduction' 
l: List α
l with 
b: ?m.4049
b 
l: List ?m.4049
l 
hl: ?m.4050 l
hl
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

nil
a ∈ destutter' R a []
α: Type u_1

l✝: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b✝, a, b: α

l: List α

hl: a ∈ destutter' R a l

cons
a ∈ destutter' R a (b :: l)
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

a ∈ destutter' R a l·
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

nil
a ∈ destutter' R a [] 
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

nil
a ∈ destutter' R a []
α: Type u_1

l✝: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b✝, a, b: α

l: List α

hl: a ∈ destutter' R a l

cons
a ∈ destutter' R a (b :: l)simp
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

a ∈ destutter' R a lrw [
α: Type u_1

l✝: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b✝, a, b: α

l: List α

hl: a ∈ destutter' R a l

cons
a ∈ destutter' R a (b :: l)
destutter': {α : Type ?u.4342} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter'
α: Type u_1

l✝: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b✝, a, b: α

l: List α

hl: a ∈ destutter' R a l

cons
a ∈ if R a b then a :: destutter' R b l else destutter' R a l]
α: Type u_1

l✝: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b✝, a, b: α

l: List α

hl: a ∈ destutter' R a l

cons
a ∈ if R a b then a :: destutter' R b l else destutter' R a l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

a ∈ destutter' R a lsplit_ifs
α: 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

cons.inl
a ∈ a :: destutter' R b l
α: 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

cons.inr
a ∈ destutter' R a l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

a ∈ destutter' R a l·
α: 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

cons.inl
a ∈ a :: destutter' R b l 
α: 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

cons.inl
a ∈ a :: destutter' R b l
α: 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

cons.inr
a ∈ destutter' R a lsimp
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

a ∈ destutter' R a l·
α: 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

cons.inr
a ∈ destutter' R a l 
α: 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

cons.inr
a ∈ destutter' R a lassumption
Goals accomplished! 🐙
#align list.mem_destutter' 
List.mem_destutter': ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] (a : α), a ∈ destutter' R a l
List.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.8293
List 
α: Type ?u.8260
α, ∀ {
a: ?m.8297
a 
b: ?m.8300
b}, 
R: α → α → Prop
R 
a: ?m.8297
a 
b: ?m.8300
b → (
l: List α
l.
destutter': {α : Type ?u.8305} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
b: ?m.8300
b).
Chain: {α : Type ?u.8346} → (α → α → Prop) → α → List α → Prop
Chain 
R: α → α → Prop
R 
a: ?m.8297
a
  | [], 
a: α
a, 
b: α
b, 
h: R a b
h => 
chain_singleton: ∀ {α : Type ?u.8411} {R : α → α → Prop} {a b : α}, Chain R a [b] ↔ R a b
chain_singleton.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr 
h: R a b
h
  | 
c: α
c :: 
l: List α
l, 
a: α
a, 
b: α
b, 
h: R a b
h => by
Goals accomplished! 🐙
    
α: 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 [
α: 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))
destutter': {α : Type ?u.8707} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter'
α: 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 (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))split_ifs with hbc
α: 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

inl
Chain R a (b :: destutter' R c l)
α: 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

inr
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 (destutter' R b (c :: l))·
α: 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

inl
Chain R a (b :: destutter' R c l) 
α: 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

inl
Chain R a (b :: destutter' R c l)
α: 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

inr
Chain R a (destutter' R b l)rw [
α: 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

inl
Chain 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 l
chain_cons
α: 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

inl
R a b ∧ Chain R b (destutter' R c l)]
α: 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

inl
R a b ∧ Chain R b (destutter' R c l)
      
α: 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

inl
Chain R a (b :: destutter' R c l)exact ⟨
h: R a b
h, 
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 c
hbc⟩
Goals accomplished! 🐙
    
α: 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))·
α: 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

inr
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

hbc: ¬R b c

inr
Chain 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 b
h
Goals 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: α → α → Prop
R 
a: ?m.9473
a).
Chain': {α : Type ?u.9517} → (α → α → Prop) → List α → Prop
Chain' 
R: α → α → Prop
R := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

Chain' R (destutter' R a l)induction' 
l: List α
l with 
b: ?m.9552
b 
l: List ?m.9552
l 
hl: ?m.9553 l
hl generalizing 
a: α
a
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝¹, b, a✝, a: α

nil
Chain' R (destutter' R a [])
α: 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: α

cons
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)·
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝¹, b, a✝, a: α

nil
Chain' R (destutter' R a []) 
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝¹, b, a✝, a: α

nil
Chain' R (destutter' R a [])
α: 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: α

cons
Chain' R (destutter' R a (b :: l))simp
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

Chain' R (destutter' R a l)rw [
α: 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: α

cons
Chain' R (destutter' R a (b :: l))
destutter': {α : Type ?u.9835} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter'
α: 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: α

cons
Chain' R (if R a b then a :: destutter' R b l else destutter' R a l)]
α: 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: α

cons
Chain' R (if R a b then a :: destutter' R b l else destutter' R a l)
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

Chain' R (destutter' R a l)split_ifs with h
α: 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

cons.inl
Chain' R (a :: destutter' R b l)
α: 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

cons.inr
Chain' R (destutter' R a l)
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

Chain' R (destutter' R a l)·
α: 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

cons.inl
Chain' R (a :: destutter' R b l) 
α: 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

cons.inl
Chain' R (a :: destutter' R b l)
α: 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

cons.inr
Chain' 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: α → α → Prop
R 
l: List ?m.9552
l 
h: R a b
h
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

Chain' R (destutter' R a l)·
α: 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

cons.inr
Chain' R (destutter' R a l) 
α: 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

cons.inr
Chain' R (destutter' R a l)exact 
hl: ?m.9553 l
hl 
a: α
a
Goals 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 :: l
destutter'_of_chain (
h: Chain R a l
h : 
l: List α
l.
Chain: {α : Type ?u.10450} → (α → α → Prop) → α → List α → Prop
Chain 
R: α → α → Prop
R 
a: α
a) : 
l: List α
l.
destutter': {α : Type ?u.10466} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: α
a = 
a: α
a :: 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: Chain R a l

destutter' R a l = a :: linduction' 
l: List α
l with 
b: ?m.10533
b 
l: List ?m.10533
l 
hb: ?m.10534 l
hb generalizing 
a: α
a
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b: α

h✝: Chain R a✝ l

a: α

h: Chain R a []

nil
destutter' R a [] = [a]
α: 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)

cons
destutter' R a (b :: l) = a :: b :: l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: Chain R a l

destutter' R a l = a :: l·
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b: α

h✝: Chain R a✝ l

a: α

h: Chain R a []

nil
destutter' R a [] = [a] 
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b: α

h✝: Chain R a✝ l

a: α

h: Chain R a []

nil
destutter' R a [] = [a]
α: 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)

cons
destutter' R a (b :: l) = a :: b :: lsimp
Goals accomplished! 🐙
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: Chain R a l

destutter' R a l = a :: lobtain 
⟨h, hc⟩: R a b ∧ Chain R b l
⟨
h: R a b
h
⟨h, hc⟩: R a b ∧ Chain R b l
, 
hc: Chain R b l
hc
⟨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 l
chain_cons.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp 
h: Chain R a (b :: l)
h
α: 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

cons.intro
destutter' R a (b :: l) = a :: b :: l
  
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

h: Chain R a l

destutter' R a l = a :: lrw [
α: 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

cons.intro
destutter' R a (b :: l) = a :: b :: l
l: List ?m.10533
l.
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 l
destutter'_cons_pos 
h: R a b
h,
α: 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

cons.intro
a :: destutter' R b l = a :: b :: l 
α: 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

cons.intro
destutter' R a (b :: l) = a :: b :: l
hb: ?m.10534 l
hb 
hc: Chain R b l
hc
α: 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

cons.intro
a :: 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 :: l
List.destutter'_of_chain

@[simp]
theorem 
destutter'_eq_self_iff: ∀ (a : α), destutter' R a l = a :: l ↔ Chain R a l
destutter'_eq_self_iff (
a: ?m.10912
a) : 
l: List α
l.
destutter': {α : Type ?u.10916} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: ?m.10912
a = 
a: ?m.10912
a :: 
l: List α
l ↔ 
l: List α
l.
Chain: {α : Type ?u.10960} → (α → α → Prop) → α → List α → Prop
Chain 
R: α → α → Prop
R 
a: ?m.10912
a :=
  ⟨fun 
h: ?m.10983
h => by
Goals accomplished! 🐙
    
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

h: destutter' R a l = a :: l

Chain R a lsuffices 
Chain': {α : Type ?u.11138} → (α → α → Prop) → List α → Prop
Chain' 
R: α → α → Prop
R (
a: α
a::
l: List α
l) by
      
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

h: destutter' R a l = a :: l

Chain R a lassumption
Goals accomplished! 🐙
    
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

h: destutter' R a l = a :: l

Chain R a lrw [
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

h: destutter' R a l = a :: l

Chain' R (a :: l)← 
h: destutter' R a l = a :: l
h
α: 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)]
α: 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)
    
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a✝, b, a: α

h: destutter' R a l = a :: l

Chain 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: α → α → Prop
R 
a: α
a
Goals accomplished! 🐙, 
destutter'_of_chain: ∀ {α : Type ?u.10989} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
  Chain R a l → destutter' R a l = a :: l
destutter'_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 l
List.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: α → α → Prop
R 
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 l
mem_destutter' 
R: α → α → Prop
R 
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.11449
List 
α: Type ?u.11415
α).
destutter: {α : Type ?u.11453} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R = 
[]: List ?m.11493
[] :=
  
rfl: ∀ {α : Sort ?u.11523} {a : α}, a = a
rfl
#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 l
destutter_cons' : (
a: α
a :: 
l: List α
l).
destutter: {α : Type ?u.11605} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R = 
destutter': {α : Type ?u.11644} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: α
a 
l: List α
l :=
  
rfl: ∀ {α : Sort ?u.11657} {a : α}, a = a
rfl
#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 l
List.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 l
destutter_cons_cons :
    (
a: α
a :: 
b: α
b :: 
l: List α
l).
destutter: {α : Type ?u.11753} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R = if 
R: α → α → Prop
R 
a: α
a 
b: α
b then 
a: α
a :: 
destutter': {α : Type ?u.11798} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
b: α
b 
l: List α
l else 
destutter': {α : Type ?u.11809} → (R : α → α → Prop) → [inst : DecidableRel R] → α → List α → List α
destutter' 
R: α → α → Prop
R 
a: α
a 
l: List α
l :=
  
rfl: ∀ {α : Sort ?u.11828} {a : α}, a = a
rfl
#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 l
List.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: α → α → Prop
R [
a: α
a] = [
a: α
a] :=
  
rfl: ∀ {α : Sort ?u.11981} {a : α}, a = a
rfl
#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: α → α → Prop
R [
a: α
a, 
b: α
b] = if 
R: α → α → Prop
R 
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 l
destutter_cons_cons 
_: List ?m.12139
_ 
R: α → α → Prop
R
#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 <+ l
destutter_sublist : ∀ 
l: List α
l : 
List: Type ?u.12263 → Type ?u.12263
List 
α: Type ?u.12230
α, 
l: List α
l.
destutter: {α : Type ?u.12268} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R <+ 
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 :: l
destutter'_sublist 
R: α → α → Prop
R 
h: α
h
#align list.destutter_sublist 
List.destutter_sublist: ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), destutter R l <+ l
List.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.12531
List 
α: Type ?u.12498
α, (
l: List α
l.
destutter: {α : Type ?u.12534} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R).
Chain': {α : Type ?u.12574} → (α → α → Prop) → List α → Prop
Chain' 
R: α → α → Prop
R
  | [] => 
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: α → α → Prop
R 
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 = l
destutter_of_chain' : ∀ 
l: List α
l : 
List: Type ?u.12869 → Type ?u.12869
List 
α: Type ?u.12836
α, 
l: List α
l.
Chain': {α : Type ?u.12873} → (α → α → Prop) → List α → Prop
Chain' 
R: α → α → Prop
R → 
l: List α
l.
destutter: {α : Type ?u.12887} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R = 
l: List α
l
  | [], _ => 
rfl: ∀ {α : Sort ?u.12968} {a : α}, a = a
rfl
  | _ :: 
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 :: l
destutter'_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 = l
List.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 l
destutter_eq_self_iff : ∀ 
l: List α
l : 
List: Type ?u.13355 → Type ?u.13355
List 
α: Type ?u.13322
α, 
l: List α
l.
destutter: {α : Type ?u.13359} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R = 
l: List α
l ↔ 
l: List α
l.
Chain': {α : Type ?u.13400} → (α → α → Prop) → List α → Prop
Chain' 
R: α → α → Prop
R
  | [] => by
Goals accomplished! 🐙 
α: Type u_1

l: List α

R: α → α → Prop

inst✝: DecidableRel R

a, b: α

destutter R [] = [] ↔ Chain' R []simp
Goals 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 l
destutter'_eq_self_iff 
R: α → α → Prop
R 
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 l
List.destutter_eq_self_iff

theorem 
destutter_idem: destutter R (destutter R l) = destutter R l
destutter_idem : (
l: List α
l.
destutter: {α : Type ?u.13873} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R).
destutter: {α : Type ?u.13913} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R = 
l: List α
l.
destutter: {α : Type ?u.13930} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R :=
  
destutter_of_chain': ∀ {α : Type ?u.13949} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), Chain' R l → destutter R l = l
destutter_of_chain' 
R: α → α → Prop
R 
_: 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: α → α → Prop
R
#align list.destutter_idem 
List.destutter_idem: ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R], destutter R (destutter R l) = destutter R l
List.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.14085
List 
α: Type ?u.14052
α}, 
destutter: {α : Type ?u.14089} → (R : α → α → Prop) → [inst : DecidableRel R] → List α → List α
destutter 
R: α → α → Prop
R 
l: List α
l = 
[]: List ?m.14124
[] ↔ 
l: List α
l = 
[]: List ?m.14155
[]
  | [] => 
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
  | _ :: 
l: List α
l => ⟨fun 
h: ?m.14244
h => 
absurd: ∀ {a : Prop} {b : Sort ?u.14246}, a → ¬a → b
absurd 
h: ?m.14244
h <| 
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: α → α → Prop
R, fun 
h: ?m.14307
h => nomatch 
h: ?m.14307
h⟩
#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