/-
Copyright (c) 2021 Yakov Pechersky. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yakov Pechersky, Chris Hughes

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

/-!
# List duplicates

## Main definitions

* `List.Duplicate x l : Prop` is an inductive property that holds when `x` is a duplicate in `l`

## Implementation details

In this file, `x ∈+ l` notation is shorthand for `List.Duplicate x l`.

-/


variable {
α: Type ?u.239
α : 
Type _: Type (?u.2+1)
Type _}

namespace List

/-- Property that an element `x : α` of `l : List α` can be found in the list more than once. -/
inductive 
Duplicate: α → List α → Prop
Duplicate (
x: α
x : 
α: Type ?u.5
α) : 
List: Type ?u.11 → Type ?u.11
List 
α: Type ?u.5
α → 
Prop: Type
Prop
  | 
cons_mem: ∀ {α : Type u_1} {x : α} {l : List α}, x ∈ l → Duplicate x (x :: l)
cons_mem {
l: List α
l : 
List: Type ?u.17 → Type ?u.17
List 
α: Type ?u.5
α} : 
x: α
x ∈ 
l: List α
l → 
Duplicate: α → List α → Prop
Duplicate 
x: α
x (
x: α
x :: 
l: List α
l)
  | 
cons_duplicate: ∀ {α : Type u_1} {x y : α} {l : List α}, Duplicate x l → Duplicate x (y :: l)
cons_duplicate {
y: α
y : 
α: Type ?u.5
α} {
l: List α
l : 
List: Type ?u.56 → Type ?u.56
List 
α: Type ?u.5
α} : 
Duplicate: α → List α → Prop
Duplicate 
x: α
x 
l: List α
l → 
Duplicate: α → List α → Prop
Duplicate 
x: α
x (
y: α
y :: 
l: List α
l)
#align list.duplicate 
List.Duplicate: {α : Type u_1} → α → List α → Prop
List.Duplicate

-- mathport name: «expr ∈+ »
local infixl:50 " ∈+ " => 
List.Duplicate: {α : Type u_1} → α → List α → Prop
List.Duplicate

variable {
l: List α
l : 
List: Type ?u.10144 → Type ?u.10144
List 
α: Type ?u.10141
α} {
x: α
x : 
α: Type ?u.12072
α}

theorem 
Mem.duplicate_cons_self: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈ l → x ∈+ x :: l
Mem.duplicate_cons_self (
h: x ∈ l
h : 
x: α
x ∈ 
l: List α
l) : 
x: α
x ∈+ 
x: α
x :: 
l: List α
l :=
  
Duplicate.cons_mem: ∀ {α : Type ?u.9087} {x : α} {l : List α}, x ∈ l → x ∈+ x :: l
Duplicate.cons_mem 
h: x ∈ l
h
#align list.mem.duplicate_cons_self 
List.Mem.duplicate_cons_self: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈ l → x ∈+ x :: l
List.Mem.duplicate_cons_self

theorem 
Duplicate.duplicate_cons: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: l
Duplicate.duplicate_cons (
h: x ∈+ l
h : 
x: α
x ∈+ 
l: List α
l) (
y: α
y : 
α: Type ?u.9103
α) : 
x: α
x ∈+ 
y: α
y :: 
l: List α
l :=
  
Duplicate.cons_duplicate: ∀ {α : Type ?u.9125} {x y : α} {l : List α}, x ∈+ l → x ∈+ y :: l
Duplicate.cons_duplicate 
h: x ∈+ l
h
#align list.duplicate.duplicate_cons 
List.Duplicate.duplicate_cons: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: l
List.Duplicate.duplicate_cons

theorem 
Duplicate.mem: x ∈+ l → x ∈ l
Duplicate.mem (
h: x ∈+ l
h : 
x: α
x ∈+ 
l: List α
l) : 
x: α
x ∈ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

h: x ∈+ l

x ∈ linduction' 
h: x ∈+ l
h with 
l': List ?m.9212
l' _ 
y: ?m.9212
y 
l': List ?m.9212
l' _ 
hm: ?m.9214 l' a✝
hm
α: Type u_1

l: List α

x: α

l': List α

a✝: x ∈ l'

cons_mem
x ∈ x :: l'
α: Type u_1

l: List α

x, y: α

l': List α

a✝: x ∈+ l'

hm: x ∈ l'

cons_duplicate
x ∈ y :: l'
  
α: Type u_1

l: List α

x: α

h: x ∈+ l

x ∈ l·
α: Type u_1

l: List α

x: α

l': List α

a✝: x ∈ l'

cons_mem
x ∈ x :: l' 
α: Type u_1

l: List α

x: α

l': List α

a✝: x ∈ l'

cons_mem
x ∈ x :: l'
α: Type u_1

l: List α

x, y: α

l': List α

a✝: x ∈+ l'

hm: x ∈ l'

cons_duplicate
x ∈ y :: l'exact 
mem_cons_self: ∀ {α : Type ?u.9236} (a : α) (l : List α), a ∈ a :: l
mem_cons_self 
_: ?m.9237
_ 
_: List ?m.9237
_
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

h: x ∈+ l

x ∈ l·
α: Type u_1

l: List α

x, y: α

l': List α

a✝: x ∈+ l'

hm: x ∈ l'

cons_duplicate
x ∈ y :: l' 
α: Type u_1

l: List α

x, y: α

l': List α

a✝: x ∈+ l'

hm: x ∈ l'

cons_duplicate
x ∈ y :: l'exact 
mem_cons_of_mem: ∀ {α : Type ?u.9249} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: l
mem_cons_of_mem 
_: ?m.9250
_ 
hm: ?m.9214 l' a✝
hm
Goals accomplished! 🐙
#align list.duplicate.mem 
List.Duplicate.mem: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → x ∈ l
List.Duplicate.mem

theorem 
Duplicate.mem_cons_self: x ∈+ x :: l → x ∈ l
Duplicate.mem_cons_self (
h: x ∈+ x :: l
h : 
x: α
x ∈+ 
x: α
x :: 
l: List α
l) : 
x: α
x ∈ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

h: x ∈+ x :: l

x ∈ lcases' 
h: x ∈+ x :: l
h with _ 
h: x ∈ l
h _ _ 
h: x ∈+ l
h
α: Type u_1

l: List α

x: α

h: x ∈ l

cons_mem
x ∈ l
α: Type u_1

l: List α

x: α

h: x ∈+ l

cons_duplicate
x ∈ l
  
α: Type u_1

l: List α

x: α

h: x ∈+ x :: l

x ∈ l·
α: Type u_1

l: List α

x: α

h: x ∈ l

cons_mem
x ∈ l 
α: Type u_1

l: List α

x: α

h: x ∈ l

cons_mem
x ∈ l
α: Type u_1

l: List α

x: α

h: x ∈+ l

cons_duplicate
x ∈ lexact 
h: x ∈ l
h
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

h: x ∈+ x :: l

x ∈ l·
α: Type u_1

l: List α

x: α

h: x ∈+ l

cons_duplicate
x ∈ l 
α: Type u_1

l: List α

x: α

h: x ∈+ l

cons_duplicate
x ∈ lexact 
h: x ∈+ l
h.
mem: ∀ {α : Type ?u.9475} {l : List α} {x : α}, x ∈+ l → x ∈ l
mem
Goals accomplished! 🐙
#align list.duplicate.mem_cons_self 
List.Duplicate.mem_cons_self: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ x :: l → x ∈ l
List.Duplicate.mem_cons_self

@[simp]
theorem 
duplicate_cons_self_iff: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ x :: l ↔ x ∈ l
duplicate_cons_self_iff : 
x: α
x ∈+ 
x: α
x :: 
l: List α
l ↔ 
x: α
x ∈ 
l: List α
l :=
  ⟨
Duplicate.mem_cons_self: ∀ {α : Type ?u.9555} {l : List α} {x : α}, x ∈+ x :: l → x ∈ l
Duplicate.mem_cons_self, 
Mem.duplicate_cons_self: ∀ {α : Type ?u.9569} {l : List α} {x : α}, x ∈ l → x ∈+ x :: l
Mem.duplicate_cons_self⟩
#align list.duplicate_cons_self_iff 
List.duplicate_cons_self_iff: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ x :: l ↔ x ∈ l
List.duplicate_cons_self_iff

theorem 
Duplicate.ne_nil: x ∈+ l → l ≠ []
Duplicate.ne_nil (
h: x ∈+ l
h : 
x: α
x ∈+ 
l: List α
l) : 
l: List α
l ≠ 
[]: List ?m.9621
[] := fun 
H: ?m.9626
H => (
mem_nil_iff: ∀ {α : Type ?u.9628} (a : α), a ∈ [] ↔ False
mem_nil_iff 
x: α
x).
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
H: ?m.9626
H ▸ 
h: x ∈+ l
h.
mem: ∀ {α : Type ?u.9634} {l : List α} {x : α}, x ∈+ l → x ∈ l
mem)
#align list.duplicate.ne_nil 
List.Duplicate.ne_nil: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → l ≠ []
List.Duplicate.ne_nil

@[simp]
theorem 
not_duplicate_nil: ∀ {α : Type u_1} (x : α), ¬x ∈+ []
not_duplicate_nil (
x: α
x : 
α: Type ?u.9662
α) : ¬
x: α
x ∈+ 
[]: List ?m.9675
[] := fun 
H: ?m.9681
H => 
H: ?m.9681
H.
ne_nil: ∀ {α : Type ?u.9683} {l : List α} {x : α}, x ∈+ l → l ≠ []
ne_nil 
rfl: ∀ {α : Sort ?u.9696} {a : α}, a = a
rfl
#align list.not_duplicate_nil 
List.not_duplicate_nil: ∀ {α : Type u_1} (x : α), ¬x ∈+ []
List.not_duplicate_nil

theorem 
Duplicate.ne_singleton: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), l ≠ [y]
Duplicate.ne_singleton (
h: x ∈+ l
h : 
x: α
x ∈+ 
l: List α
l) (
y: α
y : 
α: Type ?u.9719
α) : 
l: List α
l ≠ [
y: α
y] := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

h: x ∈+ l

y: α

l ≠ [y]induction' 
h: x ∈+ l
h with 
l': List ?m.9774
l' 
h: ?m.9775 ∈ l'
h 
z: ?m.9774
z 
l': List ?m.9774
l' 
h: ?m.9775 ∈+ l'
h _
α: Type u_1

l: List α

x, y: α

l': List α

h: x ∈ l'

cons_mem
x :: l' ≠ [y]
α: Type u_1

l: List α

x, y, z: α

l': List α

h: x ∈+ l'

a_ih✝: l' ≠ [y]

cons_duplicate
z :: l' ≠ [y]
  
α: Type u_1

l: List α

x: α

h: x ∈+ l

y: α

l ≠ [y]·
α: Type u_1

l: List α

x, y: α

l': List α

h: x ∈ l'

cons_mem
x :: l' ≠ [y] 
α: Type u_1

l: List α

x, y: α

l': List α

h: x ∈ l'

cons_mem
x :: l' ≠ [y]
α: Type u_1

l: List α

x, y, z: α

l': List α

h: x ∈+ l'

a_ih✝: l' ≠ [y]

cons_duplicate
z :: l' ≠ [y]simp [
ne_nil_of_mem: ∀ {α : Type ?u.9799} {a : α} {l : List α}, a ∈ l → l ≠ []
ne_nil_of_mem 
h: ?m.9775 ∈ l'
h]
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

h: x ∈+ l

y: α

l ≠ [y]·
α: Type u_1

l: List α

x, y, z: α

l': List α

h: x ∈+ l'

a_ih✝: l' ≠ [y]

cons_duplicate
z :: l' ≠ [y] 
α: Type u_1

l: List α

x, y, z: α

l': List α

h: x ∈+ l'

a_ih✝: l' ≠ [y]

cons_duplicate
z :: l' ≠ [y]simp [
ne_nil_of_mem: ∀ {α : Type ?u.9942} {a : α} {l : List α}, a ∈ l → l ≠ []
ne_nil_of_mem 
h: ?m.9775 ∈+ l'
h.
mem: ∀ {α : Type ?u.9946} {l : List α} {x : α}, x ∈+ l → x ∈ l
mem]
Goals accomplished! 🐙
#align list.duplicate.ne_singleton 
List.Duplicate.ne_singleton: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), l ≠ [y]
List.Duplicate.ne_singleton

@[simp]
theorem 
not_duplicate_singleton: ∀ {α : Type u_1} (x y : α), ¬x ∈+ [y]
not_duplicate_singleton (
x: α
x 
y: α
y : 
α: Type ?u.10040
α) : ¬
x: α
x ∈+ [
y: α
y] := fun 
H: ?m.10065
H => 
H: ?m.10065
H.
ne_singleton: ∀ {α : Type ?u.10067} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), l ≠ [y]
ne_singleton 
_: ?m.10074
_ 
rfl: ∀ {α : Sort ?u.10082} {a : α}, a = a
rfl
#align list.not_duplicate_singleton 
List.not_duplicate_singleton: ∀ {α : Type u_1} (x y : α), ¬x ∈+ [y]
List.not_duplicate_singleton

theorem 
Duplicate.elim_nil: ∀ {α : Type u_1} {x : α}, x ∈+ [] → False
Duplicate.elim_nil (
h: x ∈+ []
h : 
x: α
x ∈+ 
[]: List ?m.10126
[]) : 
False: Prop
False :=
  
not_duplicate_nil: ∀ {α : Type ?u.10132} (x : α), ¬x ∈+ []
not_duplicate_nil 
x: α
x 
h: x ∈+ []
h
#align list.duplicate.elim_nil 
List.Duplicate.elim_nil: ∀ {α : Type u_1} {x : α}, x ∈+ [] → False
List.Duplicate.elim_nil

theorem 
Duplicate.elim_singleton: ∀ {α : Type u_1} {x y : α}, x ∈+ [y] → False
Duplicate.elim_singleton {
y: α
y : 
α: Type ?u.10141
α} (
h: x ∈+ [y]
h : 
x: α
x ∈+ [
y: α
y]) : 
False: Prop
False :=
  
not_duplicate_singleton: ∀ {α : Type ?u.10163} (x y : α), ¬x ∈+ [y]
not_duplicate_singleton 
x: α
x 
y: α
y 
h: x ∈+ [y]
h
#align list.duplicate.elim_singleton 
List.Duplicate.elim_singleton: ∀ {α : Type u_1} {x y : α}, x ∈+ [y] → False
List.Duplicate.elim_singleton

theorem 
duplicate_cons_iff: ∀ {y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
duplicate_cons_iff {
y: α
y : 
α: Type ?u.10173
α} : 
x: α
x ∈+ 
y: α
y :: 
l: List α
l ↔ 
y: α
y = 
x: α
x ∧ 
x: α
x ∈ 
l: List α
l ∨ 
x: α
x ∈+ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x, y: α

x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ lrefine' ⟨fun 
h: ?m.10219
h => 
_: ?m.10215
_, fun 
h: ?m.10226
h => 
_: ?m.10214
_⟩
α: Type u_1

l: List α

x, y: α

h: x ∈+ y :: l

refine'_1
y = x ∧ x ∈ l ∨ x ∈+ l
α: Type u_1

l: List α

x, y: α

h: y = x ∧ x ∈ l ∨ x ∈+ l

refine'_2
x ∈+ y :: l
  
α: Type u_1

l: List α

x, y: α

x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l·
α: Type u_1

l: List α

x, y: α

h: x ∈+ y :: l

refine'_1
y = x ∧ x ∈ l ∨ x ∈+ l 
α: Type u_1

l: List α

x, y: α

h: x ∈+ y :: l

refine'_1
y = x ∧ x ∈ l ∨ x ∈+ l
α: Type u_1

l: List α

x, y: α

h: y = x ∧ x ∈ l ∨ x ∈+ l

refine'_2
x ∈+ y :: lcases' 
h: ?m.10219
h with _ 
hm: x ∈ l
hm _ _ 
hm: x ∈+ l
hm
α: Type u_1

l: List α

x: α

hm: x ∈ l

refine'_1.cons_mem
x = x ∧ x ∈ l ∨ x ∈+ l
α: Type u_1

l: List α

x, y: α

hm: x ∈+ l

refine'_1.cons_duplicate
y = x ∧ x ∈ l ∨ x ∈+ l
    
α: Type u_1

l: List α

x, y: α

h: x ∈+ y :: l

refine'_1
y = x ∧ x ∈ l ∨ x ∈+ l·
α: Type u_1

l: List α

x: α

hm: x ∈ l

refine'_1.cons_mem
x = x ∧ x ∈ l ∨ x ∈+ l 
α: Type u_1

l: List α

x: α

hm: x ∈ l

refine'_1.cons_mem
x = x ∧ x ∈ l ∨ x ∈+ l
α: Type u_1

l: List α

x, y: α

hm: x ∈+ l

refine'_1.cons_duplicate
y = x ∧ x ∈ l ∨ x ∈+ lexact 
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl ⟨
rfl: ∀ {α : Sort ?u.10423} {a : α}, a = a
rfl, 
hm: x ∈ l
hm⟩
Goals accomplished! 🐙
    
α: Type u_1

l: List α

x, y: α

h: x ∈+ y :: l

refine'_1
y = x ∧ x ∈ l ∨ x ∈+ l·
α: Type u_1

l: List α

x, y: α

hm: x ∈+ l

refine'_1.cons_duplicate
y = x ∧ x ∈ l ∨ x ∈+ l 
α: Type u_1

l: List α

x, y: α

hm: x ∈+ l

refine'_1.cons_duplicate
y = x ∧ x ∈ l ∨ x ∈+ lexact 
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr 
hm: x ∈+ l
hm
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x, y: α

x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l·
α: Type u_1

l: List α

x, y: α

h: y = x ∧ x ∈ l ∨ x ∈+ l

refine'_2
x ∈+ y :: l 
α: Type u_1

l: List α

x, y: α

h: y = x ∧ x ∈ l ∨ x ∈+ l

refine'_2
x ∈+ y :: lrcases 
h: ?m.10226
h with 
(⟨rfl | h⟩ | h): ?m.10226
(
⟨rfl | h⟩ | h: ?m.10226
⟨
rfl | h: y = x ∧ x ∈ l
rfl | h
⟨rfl | h⟩ | h: ?m.10226
⟩ | 
h: x ∈+ l
h
(⟨rfl | h⟩ | h): ?m.10226
)
α: Type u_1

l: List α

x: α

right✝: x ∈ l

refine'_2.inl.intro.refl
x ∈+ x :: l
α: Type u_1

l: List α

x, y: α

h: x ∈+ l

refine'_2.inr
x ∈+ y :: l
    
α: Type u_1

l: List α

x, y: α

h: y = x ∧ x ∈ l ∨ x ∈+ l

refine'_2
x ∈+ y :: l·
α: Type u_1

l: List α

x: α

right✝: x ∈ l

refine'_2.inl.intro.refl
x ∈+ x :: l 
α: Type u_1

l: List α

x: α

right✝: x ∈ l

refine'_2.inl.intro.refl
x ∈+ x :: l
α: Type u_1

l: List α

x, y: α

h: x ∈+ l

refine'_2.inr
x ∈+ y :: lsimpa
Goals accomplished! 🐙
    
α: Type u_1

l: List α

x, y: α

h: y = x ∧ x ∈ l ∨ x ∈+ l

refine'_2
x ∈+ y :: l·
α: Type u_1

l: List α

x, y: α

h: x ∈+ l

refine'_2.inr
x ∈+ y :: l 
α: Type u_1

l: List α

x, y: α

h: x ∈+ l

refine'_2.inr
x ∈+ y :: lexact 
h: x ∈+ l
h.
cons_duplicate: ∀ {α : Type ?u.10944} {x y : α} {l : List α}, x ∈+ l → x ∈+ y :: l
cons_duplicate
Goals accomplished! 🐙
#align list.duplicate_cons_iff 
List.duplicate_cons_iff: ∀ {α : Type u_1} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
List.duplicate_cons_iff

theorem 
Duplicate.of_duplicate_cons: ∀ {y : α}, x ∈+ y :: l → x ≠ y → x ∈+ l
Duplicate.of_duplicate_cons {
y: α
y : 
α: Type ?u.11015
α} (
h: x ∈+ y :: l
h : 
x: α
x ∈+ 
y: α
y :: 
l: List α
l) (
hx: x ≠ y
hx : 
x: α
x ≠ 
y: α
y) : 
x: α
x ∈+ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x, y: α

h: x ∈+ y :: l

hx: x ≠ y

x ∈+ lsimpa [
duplicate_cons_iff: ∀ {α : Type ?u.11044} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
duplicate_cons_iff, 
hx: x ≠ y
hx.
symm: ∀ {α : Sort ?u.11069} {a b : α}, a ≠ b → b ≠ a
symm] using 
h: x ∈+ y :: l
h
Goals accomplished! 🐙
#align list.duplicate.of_duplicate_cons 
List.Duplicate.of_duplicate_cons: ∀ {α : Type u_1} {l : List α} {x y : α}, x ∈+ y :: l → x ≠ y → x ∈+ l
List.Duplicate.of_duplicate_cons

theorem 
duplicate_cons_iff_of_ne: ∀ {y : α}, x ≠ y → (x ∈+ y :: l ↔ x ∈+ l)
duplicate_cons_iff_of_ne {
y: α
y : 
α: Type ?u.11548
α} (
hne: x ≠ y
hne : 
x: α
x ≠ 
y: α
y) : 
x: α
x ∈+ 
y: α
y :: 
l: List α
l ↔ 
x: α
x ∈+ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x, y: α

hne: x ≠ y

x ∈+ y :: l ↔ x ∈+ lsimp [
duplicate_cons_iff: ∀ {α : Type ?u.11574} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
duplicate_cons_iff, 
hne: x ≠ y
hne.
symm: ∀ {α : Sort ?u.11599} {a b : α}, a ≠ b → b ≠ a
symm]
Goals accomplished! 🐙
#align list.duplicate_cons_iff_of_ne 
List.duplicate_cons_iff_of_ne: ∀ {α : Type u_1} {l : List α} {x y : α}, x ≠ y → (x ∈+ y :: l ↔ x ∈+ l)
List.duplicate_cons_iff_of_ne

theorem 
Duplicate.mono_sublist: ∀ {α : Type u_1} {l : List α} {x : α} {l' : List α}, x ∈+ l → l <+ l' → x ∈+ l'
Duplicate.mono_sublist {
l': List α
l' : 
List: Type ?u.12080 → Type ?u.12080
List 
α: Type ?u.12072
α} (
hx: x ∈+ l
hx : 
x: α
x ∈+ 
l: List α
l) (
h: l <+ l'
h : 
l: List α
l <+ 
l': List α
l') : 
x: α
x ∈+ 
l': List α
l' := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

l': List α

hx: x ∈+ l

h: l <+ l'

x ∈+ l'induction' 
h: l <+ l'
h with 
l₁: List ?m.12136
l₁ 
l₂: List ?m.12136
l₂ 
y: ?m.12136
y _ 
IH: ?m.12137 l₁ l₂ a✝
IH 
l₁: List ?m.12136
l₁ 
l₂: List ?m.12136
l₂ 
y: ?m.12136
y 
h: l₁ <+ l₂
h 
IH: ?m.12137 l₁ l₂ h
IH
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

hx: x ∈+ []

slnil
x ∈+ []
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

a✝: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons
x ∈+ y :: l₂
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂
  
α: Type u_1

l: List α

x: α

l': List α

hx: x ∈+ l

h: l <+ l'

x ∈+ l'·
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

hx: x ∈+ []

slnil
x ∈+ [] 
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

hx: x ∈+ []

slnil
x ∈+ []
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

a✝: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons
x ∈+ y :: l₂
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂exact 
hx: x ∈+ []
hx
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

l': List α

hx: x ∈+ l

h: l <+ l'

x ∈+ l'·
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

a✝: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons
x ∈+ y :: l₂ 
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

a✝: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons
x ∈+ y :: l₂
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂exact (
IH: ?m.12137 l₁ l₂ a✝
IH 
hx: x ∈+ l₁
hx).
duplicate_cons: ∀ {α : Type ?u.12177} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: l
duplicate_cons 
_: ?m.12183
_
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

l': List α

hx: x ∈+ l

h: l <+ l'

x ∈+ l'·
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂ 
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂rw [
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂
duplicate_cons_iff: ∀ {α : Type ?u.12193} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
duplicate_cons_iff
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: y = x ∧ x ∈ l₁ ∨ x ∈+ l₁

cons₂
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂]
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: y = x ∧ x ∈ l₁ ∨ x ∈+ l₁

cons₂
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂ at 
hx: x ∈+ y :: l₁
hx⊢
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: y = x ∧ x ∈ l₁ ∨ x ∈+ l₁

cons₂
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
    
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂rcases 
hx: y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
hx with 
(⟨rfl, hx⟩ | hx): y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
(
⟨rfl, hx⟩: y = x ∧ x ∈ l₁
⟨
rfl: y = x
rfl
⟨rfl, hx⟩: y = x ∧ x ∈ l₁
, 
hx: unknown free variable '_uniq.12279'
hx
⟨rfl, hx⟩: y = x ∧ x ∈ l₁
⟩
⟨rfl, hx⟩ | hx: y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
 | 
hx: x ∈+ l₁
hx
(⟨rfl, hx⟩ | hx): y = x ∧ x ∈ l₁ ∨ x ∈+ l₁
)
α: Type u_1

l, l', l₁, l₂: List α

y: α

h: l₁ <+ l₂

hx✝: y ∈+ l

IH: y ∈+ l₁ → y ∈+ l₂

hx: y ∈ l₁

cons₂.inl.intro
y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons₂.inr
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
    
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂·
α: Type u_1

l, l', l₁, l₂: List α

y: α

h: l₁ <+ l₂

hx✝: y ∈+ l

IH: y ∈+ l₁ → y ∈+ l₂

hx: y ∈ l₁

cons₂.inl.intro
y = y ∧ y ∈ l₂ ∨ y ∈+ l₂ 
α: Type u_1

l, l', l₁, l₂: List α

y: α

h: l₁ <+ l₂

hx✝: y ∈+ l

IH: y ∈+ l₁ → y ∈+ l₂

hx: y ∈ l₁

cons₂.inl.intro
y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons₂.inr
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂simp [
h: l₁ <+ l₂
h.
subset: ∀ {α : Type ?u.12302} {l₁ l₂ : List α}, l₁ <+ l₂ → l₁ ⊆ l₂
subset 
hx: y ∈ l₁
hx]
Goals accomplished! 🐙
    
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ y :: l₁

cons₂
x ∈+ y :: l₂·
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons₂.inr
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂ 
α: Type u_1

l: List α

x: α

l': List α

hx✝: x ∈+ l

l₁, l₂: List α

y: α

h: l₁ <+ l₂

IH: x ∈+ l₁ → x ∈+ l₂

hx: x ∈+ l₁

cons₂.inr
y = x ∧ x ∈ l₂ ∨ x ∈+ l₂simp [
IH: ?m.12137 l₁ l₂ h
IH 
hx: x ∈+ l₁
hx]
Goals accomplished! 🐙
#align list.duplicate.mono_sublist 
List.Duplicate.mono_sublist: ∀ {α : Type u_1} {l : List α} {x : α} {l' : List α}, x ∈+ l → l <+ l' → x ∈+ l'
List.Duplicate.mono_sublist

/-- The contrapositive of `List.nodup_iff_sublist`. -/
theorem 
duplicate_iff_sublist: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ l
duplicate_iff_sublist : 
x: α
x ∈+ 
l: List α
l ↔ [
x: α
x, 
x: α
x] <+ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

x ∈+ l ↔ [x, x] <+ linduction' 
l: List α
l with 
y: ?m.13175
y 
l: List ?m.13175
l 
IH: ?m.13176 l
IH
α: Type u_1

l: List α

x: α

nil
x ∈+ [] ↔ [x, x] <+ []
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

cons
x ∈+ y :: l ↔ [x, x] <+ y :: l
  
α: Type u_1

l: List α

x: α

x ∈+ l ↔ [x, x] <+ l·
α: Type u_1

l: List α

x: α

nil
x ∈+ [] ↔ [x, x] <+ [] 
α: Type u_1

l: List α

x: α

nil
x ∈+ [] ↔ [x, x] <+ []
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

cons
x ∈+ y :: l ↔ [x, x] <+ y :: lsimp
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

x ∈+ l ↔ [x, x] <+ l·
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

cons
x ∈+ y :: l ↔ [x, x] <+ y :: l 
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

cons
x ∈+ y :: l ↔ [x, x] <+ y :: lby_cases 
hx: ?m.13361
hx : 
x: α
x = 
y: ?m.13175
y
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: x = y

pos
x ∈+ y :: l ↔ [x, x] <+ y :: l
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: l
    
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

cons
x ∈+ y :: l ↔ [x, x] <+ y :: l·
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: x = y

pos
x ∈+ y :: l ↔ [x, x] <+ y :: l 
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: x = y

pos
x ∈+ y :: l ↔ [x, x] <+ y :: l
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: lsimp [
hx: ?m.13354
hx, 
cons_sublist_cons_iff: ∀ {α : Type ?u.13369} {l₁ l₂ : List α} {a : α}, a :: l₁ <+ a :: l₂ ↔ l₁ <+ l₂
cons_sublist_cons_iff, 
singleton_sublist: ∀ {α : Type ?u.13393} {a : α} {l : List α}, [a] <+ l ↔ a ∈ l
singleton_sublist]
Goals accomplished! 🐙
    
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

cons
x ∈+ y :: l ↔ [x, x] <+ y :: l·
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: l 
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: lrw [
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: l
duplicate_cons_iff_of_ne: ∀ {α : Type ?u.14200} {l : List α} {x y : α}, x ≠ y → (x ∈+ y :: l ↔ x ∈+ l)
duplicate_cons_iff_of_ne 
hx: ?m.13361
hx,
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ l ↔ [x, x] <+ y :: l 
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: l
IH: ?m.13176 l
IH
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
[x, x] <+ l ↔ [x, x] <+ y :: l]
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
[x, x] <+ l ↔ [x, x] <+ y :: l
      
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: lrefine' ⟨
sublist_cons_of_sublist: ∀ {α : Type ?u.14234} (a : α) {l₁ l₂ : List α}, l₁ <+ l₂ → l₁ <+ a :: l₂
sublist_cons_of_sublist 
y: ?m.13175
y, fun 
h: ?m.14245
h => 
_: ?m.14230
_⟩
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

h: [x, x] <+ y :: l

neg
[x, x] <+ l
      
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: lcases 
h: ?m.14245
h
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

a✝: [x, x] <+ l

neg.cons
[x, x] <+ l
α: Type u_1

l✝: List α

x: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = x

a✝: [x] <+ l

neg.cons₂
[x, x] <+ l
      
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: l·
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

a✝: [x, x] <+ l

neg.cons
[x, x] <+ l 
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

a✝: [x, x] <+ l

neg.cons
[x, x] <+ l
α: Type u_1

l✝: List α

x: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = x

a✝: [x] <+ l

neg.cons₂
[x, x] <+ lassumption
Goals accomplished! 🐙
      
α: Type u_1

l✝: List α

x, y: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = y

neg
x ∈+ y :: l ↔ [x, x] <+ y :: l·
α: Type u_1

l✝: List α

x: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = x

a✝: [x] <+ l

neg.cons₂
[x, x] <+ l 
α: Type u_1

l✝: List α

x: α

l: List α

IH: x ∈+ l ↔ [x, x] <+ l

hx: ¬x = x

a✝: [x] <+ l

neg.cons₂
[x, x] <+ lcontradiction
Goals accomplished! 🐙
#align list.duplicate_iff_sublist 
List.duplicate_iff_sublist: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ l
List.duplicate_iff_sublist

theorem 
nodup_iff_forall_not_duplicate: Nodup l ↔ ∀ (x : α), ¬x ∈+ l
nodup_iff_forall_not_duplicate : 
Nodup: {α : Type ?u.14605} → List α → Prop
Nodup 
l: List α
l ↔ ∀ 
x: α
x : 
α: Type ?u.14597
α, ¬
x: α
x ∈+ 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

Nodup l ↔ ∀ (x : α), ¬x ∈+ lsimp_rw [
α: Type u_1

l: List α

x: α

Nodup l ↔ ∀ (x : α), ¬x ∈+ l
nodup_iff_sublist: ∀ {α : Type ?u.14658} {l : List α}, Nodup l ↔ ∀ (a : α), ¬[a, a] <+ l
nodup_iff_sublist,
α: Type u_1

l: List α

x: α

(∀ (a : α), ¬[a, a] <+ l) ↔ ∀ (x : α), ¬x ∈+ l 
α: Type u_1

l: List α

x: α

Nodup l ↔ ∀ (x : α), ¬x ∈+ l
duplicate_iff_sublist: ∀ {α : Type ?u.14754} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ l
duplicate_iff_sublist
Goals accomplished! 🐙]
Goals accomplished! 🐙
#align list.nodup_iff_forall_not_duplicate 
List.nodup_iff_forall_not_duplicate: ∀ {α : Type u_1} {l : List α}, Nodup l ↔ ∀ (x : α), ¬x ∈+ l
List.nodup_iff_forall_not_duplicate

theorem 
exists_duplicate_iff_not_nodup: ∀ {α : Type u_1} {l : List α}, (∃ x, x ∈+ l) ↔ ¬Nodup l
exists_duplicate_iff_not_nodup : (∃ 
x: α
x : 
α: Type ?u.14847
α, 
x: α
x ∈+ 
l: List α
l) ↔ ¬
Nodup: {α : Type ?u.14864} → List α → Prop
Nodup 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

(∃ x, x ∈+ l) ↔ ¬Nodup lsimp [
nodup_iff_forall_not_duplicate: ∀ {α : Type ?u.14869} {l : List α}, Nodup l ↔ ∀ (x : α), ¬x ∈+ l
nodup_iff_forall_not_duplicate]
Goals accomplished! 🐙
#align list.exists_duplicate_iff_not_nodup 
List.exists_duplicate_iff_not_nodup: ∀ {α : Type u_1} {l : List α}, (∃ x, x ∈+ l) ↔ ¬Nodup l
List.exists_duplicate_iff_not_nodup

theorem 
Duplicate.not_nodup: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ¬Nodup l
Duplicate.not_nodup (
h: x ∈+ l
h : 
x: α
x ∈+ 
l: List α
l) : ¬
Nodup: {α : Type ?u.16250} → List α → Prop
Nodup 
l: List α
l := fun 
H: ?m.16257
H =>
  
nodup_iff_forall_not_duplicate: ∀ {α : Type ?u.16259} {l : List α}, Nodup l ↔ ∀ (x : α), ¬x ∈+ l
nodup_iff_forall_not_duplicate.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp 
H: ?m.16257
H 
_: ?m.16260
_ 
h: x ∈+ l
h
#align list.duplicate.not_nodup 
List.Duplicate.not_nodup: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ¬Nodup l
List.Duplicate.not_nodup

theorem 
duplicate_iff_two_le_count: ∀ [inst : DecidableEq α], x ∈+ l ↔ 2 ≤ count x l
duplicate_iff_two_le_count [
DecidableEq: Sort ?u.16290 → Sort (max1?u.16290)
DecidableEq 
α: Type ?u.16282
α] : 
x: α
x ∈+ 
l: List α
l ↔ 
2: ?m.16304
2 ≤ 
count: {α : Type ?u.16317} → [inst : BEq α] → α → List α → ℕ
count 
x: α
x 
l: List α
l := by
Goals accomplished! 🐙
  
α: Type u_1

l: List α

x: α

inst✝: DecidableEq α

x ∈+ l ↔ 2 ≤ count x lsimp [
duplicate_iff_sublist: ∀ {α : Type ?u.16376} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ l
duplicate_iff_sublist, 
le_count_iff_replicate_sublist: ∀ {α : Type ?u.16394} {l : List α} [inst : DecidableEq α] {n : ℕ} {a : α}, n ≤ count a l ↔ replicate n a <+ l
le_count_iff_replicate_sublist]
Goals accomplished! 🐙
#align list.duplicate_iff_two_le_count 
List.duplicate_iff_two_le_count: ∀ {α : Type u_1} {l : List α} {x : α} [inst : DecidableEq α], x ∈+ l ↔ 2 ≤ count x l
List.duplicate_iff_two_le_count

instance 
decidableDuplicate: [inst : DecidableEq α] → (x : α) → (l : List α) → Decidable (x ∈+ l)
decidableDuplicate [
DecidableEq: Sort ?u.17733 → Sort (max1?u.17733)
DecidableEq 
α: Type ?u.17725
α] (
x: α
x : 
α: Type ?u.17725
α) : ∀ 
l: List α
l : 
List: Type ?u.17745 → Type ?u.17745
List 
α: Type ?u.17725
α, 
Decidable: Prop → Type
Decidable (
x: α
x ∈+ 
l: List α
l)
  | [] => 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse (
not_duplicate_nil: ∀ {α : Type ?u.17772} (x : α), ¬x ∈+ []
not_duplicate_nil 
x: α
x)
  | 
y: α
y :: 
l: List α
l =>
    match 
decidableDuplicate: [inst : DecidableEq α] → (x : α) → (l : List α) → Decidable (x ∈+ l)
decidableDuplicate 
x: α
x 
l: List α
l with
    | 
isTrue: {p : Prop} → p → Decidable p
isTrue 
h: x ∈+ l
h => 
isTrue: {p : Prop} → p → Decidable p
isTrue (
h: x ∈+ l
h.
duplicate_cons: ∀ {α : Type ?u.17844} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: l
duplicate_cons 
y: α
y)
    | 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse 
h: ¬x ∈+ l
h =>
      if 
hx: ?m.17977
hx : 
y: α
y = 
x: α
x ∧ 
x: α
x ∈ 
l: List α
l then 
isTrue: {p : Prop} → p → Decidable p
isTrue (
hx: ?m.17941
hx.
left: ∀ {a b : Prop}, a ∧ b → a
left.
symm: ∀ {α : Sort ?u.17948} {a b : α}, a = b → b = a
symm ▸ 
List.Mem.duplicate_cons_self: ∀ {α : Type ?u.17959} {l : List α} {x : α}, x ∈ l → x ∈+ x :: l
List.Mem.duplicate_cons_self 
hx: ?m.17941
hx.
right: ∀ {a b : Prop}, a ∧ b → b
right)
      else 
isFalse: {p : Prop} → ¬p → Decidable p
isFalse (by
Goals accomplished! 🐙 
α: Type ?u.17725

l✝: List α

x✝: α

inst✝: DecidableEq α

x, y: α

l: List α

h: ¬x ∈+ l

hx: ¬(y = x ∧ x ∈ l)

¬x ∈+ y :: lsimpa [
duplicate_cons_iff: ∀ {α : Type ?u.18137} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
duplicate_cons_iff, 
h: ¬x ∈+ l
h] using 
hx: ¬(y = x ∧ x ∈ l)
hx
Goals accomplished! 🐙)
#align list.decidable_duplicate 
List.decidableDuplicate: {α : Type u_1} → [inst : DecidableEq α] → (x : α) → (l : List α) → Decidable (x ∈+ l)
List.decidableDuplicate

end List