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: Yakov Pechersky, Chris Hughes

! This file was ported from Lean 3 source module data.list.duplicate
! 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 α → PropDuplicate (x: αx : α: Type ?u.5α) : List: Type ?u.11 → Type ?u.11List α: Type ?u.5α → Prop: TypeProp
| 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.17List α: Type ?u.5α} : x: αx ∈ l: List αl → Duplicate: α → List α → PropDuplicate 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.56List α: Type ?u.5α} : Duplicate: α → List α → PropDuplicate x: αx l: List αl → Duplicate: α → List α → PropDuplicate x: αx (y: αy :: l: List αl)
#align list.duplicate List.Duplicate: {α : Type u_1} → α → List α → PropList.Duplicate

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

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

theorem Mem.duplicate_cons_self: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈ l → x ∈+ x :: lMem.duplicate_cons_self (h: x ∈ lh : 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 :: lDuplicate.cons_mem h: x ∈ lh
#align list.mem.duplicate_cons_self List.Mem.duplicate_cons_self: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈ l → x ∈+ x :: lList.Mem.duplicate_cons_self

theorem Duplicate.duplicate_cons: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: lDuplicate.duplicate_cons (h: x ∈+ lh : 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 :: lDuplicate.cons_duplicate h: x ∈+ lh
#align list.duplicate.duplicate_cons List.Duplicate.duplicate_cons: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: lList.Duplicate.duplicate_cons

theorem Duplicate.mem: x ∈+ l → x ∈ lDuplicate.mem (h: x ∈+ lh : x: αx ∈+ l: List αl) : x: αx ∈ l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx: αh: x ∈+ lx ∈ linduction' h: x ∈+ lh with l': List ?m.9212l' _ y: ?m.9212y l': List ?m.9212l' _ hm: ?m.9214 l' a✝hmα: Type u_1l: List αx: αl': List αa✝: x ∈ l'cons_memx ∈ x :: l'α: Type u_1l: List αx, y: αl': List αa✝: x ∈+ l'hm: x ∈ l'cons_duplicatex ∈ y :: l'
α: Type u_1l: List αx: αh: x ∈+ lx ∈ l·α: Type u_1l: List αx: αl': List αa✝: x ∈ l'cons_memx ∈ x :: l' α: Type u_1l: List αx: αl': List αa✝: x ∈ l'cons_memx ∈ x :: l'α: Type u_1l: List αx, y: αl': List αa✝: x ∈+ l'hm: x ∈ l'cons_duplicatex ∈ y :: l'exact mem_cons_self: ∀ {α : Type ?u.9236} (a : α) (l : List α), a ∈ a :: lmem_cons_self _: ?m.9237_ _: List ?m.9237_Goals accomplished! 🐙
α: Type u_1l: List αx: αh: x ∈+ lx ∈ l·α: Type u_1l: List αx, y: αl': List αa✝: x ∈+ l'hm: x ∈ l'cons_duplicatex ∈ y :: l' α: Type u_1l: List αx, y: αl': List αa✝: x ∈+ l'hm: x ∈ l'cons_duplicatex ∈ y :: l'exact mem_cons_of_mem: ∀ {α : Type ?u.9249} (y : α) {a : α} {l : List α}, a ∈ l → a ∈ y :: lmem_cons_of_mem _: ?m.9250_ hm: ?m.9214 l' a✝hmGoals accomplished! 🐙
#align list.duplicate.mem List.Duplicate.mem: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l → x ∈ lList.Duplicate.mem

theorem Duplicate.mem_cons_self: x ∈+ x :: l → x ∈ lDuplicate.mem_cons_self (h: x ∈+ x :: lh : x: αx ∈+ x: αx :: l: List αl) : x: αx ∈ l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx: αh: x ∈+ x :: lx ∈ lcases' h: x ∈+ x :: lh with _ h: x ∈ lh _ _ h: x ∈+ lhα: Type u_1l: List αx: αh: x ∈ lcons_memx ∈ lα: Type u_1l: List αx: αh: x ∈+ lcons_duplicatex ∈ l
α: Type u_1l: List αx: αh: x ∈+ x :: lx ∈ l·α: Type u_1l: List αx: αh: x ∈ lcons_memx ∈ l α: Type u_1l: List αx: αh: x ∈ lcons_memx ∈ lα: Type u_1l: List αx: αh: x ∈+ lcons_duplicatex ∈ lexact h: x ∈ lhGoals accomplished! 🐙
α: Type u_1l: List αx: αh: x ∈+ x :: lx ∈ l·α: Type u_1l: List αx: αh: x ∈+ lcons_duplicatex ∈ l α: Type u_1l: List αx: αh: x ∈+ lcons_duplicatex ∈ lexact h: x ∈+ lh.mem: ∀ {α : Type ?u.9475} {l : List α} {x : α}, x ∈+ l → x ∈ lmemGoals accomplished! 🐙
#align list.duplicate.mem_cons_self List.Duplicate.mem_cons_self: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ x :: l → x ∈ lList.Duplicate.mem_cons_self

@[simp]
theorem duplicate_cons_self_iff: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ x :: l ↔ x ∈ lduplicate_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 ∈ lDuplicate.mem_cons_self, Mem.duplicate_cons_self: ∀ {α : Type ?u.9569} {l : List α} {x : α}, x ∈ l → x ∈+ x :: lMem.duplicate_cons_self⟩
#align list.duplicate_cons_self_iff List.duplicate_cons_self_iff: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ x :: l ↔ x ∈ lList.duplicate_cons_self_iff

theorem Duplicate.ne_nil: x ∈+ l → l ≠ []Duplicate.ne_nil (h: x ∈+ lh : x: αx ∈+ l: List αl) : l: List αl ≠ []: List ?m.9621[] := fun H: ?m.9626H => (mem_nil_iff: ∀ {α : Type ?u.9628} (a : α), a ∈ [] ↔ Falsemem_nil_iff x: αx).mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (H: ?m.9626H ▸ h: x ∈+ lh.mem: ∀ {α : Type ?u.9634} {l : List α} {x : α}, x ∈+ l → x ∈ lmem)
#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.9681H => H: ?m.9681H.ne_nil: ∀ {α : Type ?u.9683} {l : List α} {x : α}, x ∈+ l → l ≠ []ne_nil rfl: ∀ {α : Sort ?u.9696} {a : α}, a = arfl
#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 ∈+ lh : x: αx ∈+ l: List αl) (y: αy : α: Type ?u.9719α) : l: List αl ≠ [y: αy] := byGoals accomplished! 🐙
α: Type u_1l: List αx: αh: x ∈+ ly: αl ≠ [y]induction' h: x ∈+ lh with l': List ?m.9774l' h: ?m.9775 ∈ l'h z: ?m.9774z l': List ?m.9774l' h: ?m.9775 ∈+ l'h _α: Type u_1l: List αx, y: αl': List αh: x ∈ l'cons_memx :: l' ≠ [y]α: Type u_1l: List αx, y, z: αl': List αh: x ∈+ l'a_ih✝: l' ≠ [y]cons_duplicatez :: l' ≠ [y]
α: Type u_1l: List αx: αh: x ∈+ ly: αl ≠ [y]·α: Type u_1l: List αx, y: αl': List αh: x ∈ l'cons_memx :: l' ≠ [y] α: Type u_1l: List αx, y: αl': List αh: x ∈ l'cons_memx :: l' ≠ [y]α: Type u_1l: List αx, y, z: αl': List αh: x ∈+ l'a_ih✝: l' ≠ [y]cons_duplicatez :: 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_1l: List αx: αh: x ∈+ ly: αl ≠ [y]·α: Type u_1l: List αx, y, z: αl': List αh: x ∈+ l'a_ih✝: l' ≠ [y]cons_duplicatez :: l' ≠ [y] α: Type u_1l: List αx, y, z: αl': List αh: x ∈+ l'a_ih✝: l' ≠ [y]cons_duplicatez :: 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 ∈ lmem]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.10065H => H: ?m.10065H.ne_singleton: ∀ {α : Type ?u.10067} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), l ≠ [y]ne_singleton _: ?m.10074_ rfl: ∀ {α : Sort ?u.10082} {a : α}, a = arfl
#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 ∈+ [] → FalseDuplicate.elim_nil (h: x ∈+ []h : x: αx ∈+ []: List ?m.10126[]) : False: PropFalse :=
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 ∈+ [] → FalseList.Duplicate.elim_nil

theorem Duplicate.elim_singleton: ∀ {α : Type u_1} {x y : α}, x ∈+ [y] → FalseDuplicate.elim_singleton {y: αy : α: Type ?u.10141α} (h: x ∈+ [y]h : x: αx ∈+ [y: αy]) : False: PropFalse :=
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] → FalseList.Duplicate.elim_singleton

theorem duplicate_cons_iff: ∀ {y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ lduplicate_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 := byGoals accomplished! 🐙
α: Type u_1l: List αx, y: αx ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ lrefine' ⟨fun h: ?m.10219h => _: ?m.10215_, fun h: ?m.10226h => _: ?m.10214_⟩α: Type u_1l: List αx, y: αh: x ∈+ y :: lrefine'_1y = x ∧ x ∈ l ∨ x ∈+ lα: Type u_1l: List αx, y: αh: y = x ∧ x ∈ l ∨ x ∈+ lrefine'_2x ∈+ y :: l
α: Type u_1l: List αx, y: αx ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l·α: Type u_1l: List αx, y: αh: x ∈+ y :: lrefine'_1y = x ∧ x ∈ l ∨ x ∈+ l α: Type u_1l: List αx, y: αh: x ∈+ y :: lrefine'_1y = x ∧ x ∈ l ∨ x ∈+ lα: Type u_1l: List αx, y: αh: y = x ∧ x ∈ l ∨ x ∈+ lrefine'_2x ∈+ y :: lcases' h: ?m.10219h with _ hm: x ∈ lhm _ _ hm: x ∈+ lhmα: Type u_1l: List αx: αhm: x ∈ lrefine'_1.cons_memx = x ∧ x ∈ l ∨ x ∈+ lα: Type u_1l: List αx, y: αhm: x ∈+ lrefine'_1.cons_duplicatey = x ∧ x ∈ l ∨ x ∈+ l
α: Type u_1l: List αx, y: αh: x ∈+ y :: lrefine'_1y = x ∧ x ∈ l ∨ x ∈+ l·α: Type u_1l: List αx: αhm: x ∈ lrefine'_1.cons_memx = x ∧ x ∈ l ∨ x ∈+ l α: Type u_1l: List αx: αhm: x ∈ lrefine'_1.cons_memx = x ∧ x ∈ l ∨ x ∈+ lα: Type u_1l: List αx, y: αhm: x ∈+ lrefine'_1.cons_duplicatey = x ∧ x ∈ l ∨ x ∈+ lexact Or.inl: ∀ {a b : Prop}, a → a ∨ bOr.inl ⟨rfl: ∀ {α : Sort ?u.10423} {a : α}, a = arfl, hm: x ∈ lhm⟩Goals accomplished! 🐙
α: Type u_1l: List αx, y: αh: x ∈+ y :: lrefine'_1y = x ∧ x ∈ l ∨ x ∈+ l·α: Type u_1l: List αx, y: αhm: x ∈+ lrefine'_1.cons_duplicatey = x ∧ x ∈ l ∨ x ∈+ l α: Type u_1l: List αx, y: αhm: x ∈+ lrefine'_1.cons_duplicatey = x ∧ x ∈ l ∨ x ∈+ lexact Or.inr: ∀ {a b : Prop}, b → a ∨ bOr.inr hm: x ∈+ lhmGoals accomplished! 🐙
α: Type u_1l: List αx, y: αx ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l·α: Type u_1l: List αx, y: αh: y = x ∧ x ∈ l ∨ x ∈+ lrefine'_2x ∈+ y :: l α: Type u_1l: List αx, y: αh: y = x ∧ x ∈ l ∨ x ∈+ lrefine'_2x ∈+ y :: lrcases h: ?m.10226h with (⟨rfl | h⟩ | h): ?m.10226(⟨rfl | h⟩ | h: ?m.10226⟨rfl | h: y = x ∧ x ∈ lrfl | h⟨rfl | h⟩ | h: ?m.10226⟩ | h: x ∈+ lh(⟨rfl | h⟩ | h): ?m.10226)α: Type u_1l: List αx: αright✝: x ∈ lrefine'_2.inl.intro.reflx ∈+ x :: lα: Type u_1l: List αx, y: αh: x ∈+ lrefine'_2.inrx ∈+ y :: l
α: Type u_1l: List αx, y: αh: y = x ∧ x ∈ l ∨ x ∈+ lrefine'_2x ∈+ y :: l·α: Type u_1l: List αx: αright✝: x ∈ lrefine'_2.inl.intro.reflx ∈+ x :: l α: Type u_1l: List αx: αright✝: x ∈ lrefine'_2.inl.intro.reflx ∈+ x :: lα: Type u_1l: List αx, y: αh: x ∈+ lrefine'_2.inrx ∈+ y :: lsimpaGoals accomplished! 🐙
α: Type u_1l: List αx, y: αh: y = x ∧ x ∈ l ∨ x ∈+ lrefine'_2x ∈+ y :: l·α: Type u_1l: List αx, y: αh: x ∈+ lrefine'_2.inrx ∈+ y :: l α: Type u_1l: List αx, y: αh: x ∈+ lrefine'_2.inrx ∈+ y :: lexact h: x ∈+ lh.cons_duplicate: ∀ {α : Type ?u.10944} {x y : α} {l : List α}, x ∈+ l → x ∈+ y :: lcons_duplicateGoals 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 ∈+ lList.duplicate_cons_iff

theorem Duplicate.of_duplicate_cons: ∀ {y : α}, x ∈+ y :: l → x ≠ y → x ∈+ lDuplicate.of_duplicate_cons {y: αy : α: Type ?u.11015α} (h: x ∈+ y :: lh : x: αx ∈+ y: αy :: l: List αl) (hx: x ≠ yhx : x: αx ≠ y: αy) : x: αx ∈+ l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx, y: αh: x ∈+ y :: lhx: x ≠ yx ∈+ lsimpa [duplicate_cons_iff: ∀ {α : Type ?u.11044} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ lduplicate_cons_iff, hx: x ≠ yhx.symm: ∀ {α : Sort ?u.11069} {a b : α}, a ≠ b → b ≠ asymm] using h: x ∈+ y :: lhGoals 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 ∈+ lList.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 ≠ yhne : x: αx ≠ y: αy) : x: αx ∈+ y: αy :: l: List αl ↔ x: αx ∈+ l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx, y: αhne: x ≠ yx ∈+ y :: l ↔ x ∈+ lsimp [duplicate_cons_iff: ∀ {α : Type ?u.11574} {l : List α} {x y : α}, x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ lduplicate_cons_iff, hne: x ≠ yhne.symm: ∀ {α : Sort ?u.11599} {a b : α}, a ≠ b → b ≠ asymm]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.12080List α: Type ?u.12072α} (hx: x ∈+ lhx : x: αx ∈+ l: List αl) (h: l <+ l'h : l: List αl <+ l': List αl') : x: αx ∈+ l': List αl' := byGoals accomplished! 🐙
α: Type u_1l: List αx: αl': List αhx: x ∈+ lh: l <+ l'x ∈+ l'induction' h: l <+ l'h with l₁: List ?m.12136l₁ l₂: List ?m.12136l₂ y: ?m.12136y _ IH: ?m.12137 l₁ l₂ a✝IH l₁: List ?m.12136l₁ l₂: List ?m.12136l₂ y: ?m.12136y h: l₁ <+ l₂h IH: ?m.12137 l₁ l₂ hIHα: Type u_1l: List αx: αl': List αhx✝: x ∈+ lhx: x ∈+ []slnilx ∈+ []α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αa✝: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁consx ∈+ y :: l₂α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ y :: l₁cons₂x ∈+ y :: l₂
α: Type u_1l: List αx: αl': List αhx: x ∈+ lh: l <+ l'x ∈+ l'·α: Type u_1l: List αx: αl': List αhx✝: x ∈+ lhx: x ∈+ []slnilx ∈+ [] α: Type u_1l: List αx: αl': List αhx✝: x ∈+ lhx: x ∈+ []slnilx ∈+ []α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αa✝: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁consx ∈+ y :: l₂α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ y :: l₁cons₂x ∈+ y :: l₂exact hx: x ∈+ []hxGoals accomplished! 🐙
α: Type u_1l: List αx: αl': List αhx: x ∈+ lh: l <+ l'x ∈+ l'·α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αa✝: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁consx ∈+ y :: l₂ α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αa✝: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁consx ∈+ y :: l₂α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, 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 :: lduplicate_cons _: ?m.12183_Goals accomplished! 🐙
α: Type u_1l: List αx: αl': List αhx: x ∈+ lh: l <+ l'x ∈+ l'·α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ y :: l₁cons₂x ∈+ y :: l₂ α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ y :: l₁cons₂x ∈+ y :: l₂rw [α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, 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 ∈+ lduplicate_cons_iffα: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, 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_1l: List αx: αl': List αhx✝: x ∈+ ll₁, 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_1l: List αx: αl': List αhx✝: x ∈+ ll₁, 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_1l: List αx: αl': List αhx✝: x ∈+ ll₁, 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 = xrfl⟨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_1l, l', l₁, l₂: List αy: αh: l₁ <+ l₂hx✝: y ∈+ lIH: y ∈+ l₁ → y ∈+ l₂hx: y ∈ l₁cons₂.inl.introy = y ∧ y ∈ l₂ ∨ y ∈+ l₂α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁cons₂.inry = x ∧ x ∈ l₂ ∨ x ∈+ l₂
α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ y :: l₁cons₂x ∈+ y :: l₂·α: Type u_1l, l', l₁, l₂: List αy: αh: l₁ <+ l₂hx✝: y ∈+ lIH: y ∈+ l₁ → y ∈+ l₂hx: y ∈ l₁cons₂.inl.introy = y ∧ y ∈ l₂ ∨ y ∈+ l₂ α: Type u_1l, l', l₁, l₂: List αy: αh: l₁ <+ l₂hx✝: y ∈+ lIH: y ∈+ l₁ → y ∈+ l₂hx: y ∈ l₁cons₂.inl.introy = y ∧ y ∈ l₂ ∨ y ∈+ l₂α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁cons₂.inry = 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_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ y :: l₁cons₂x ∈+ y :: l₂·α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁cons₂.inry = x ∧ x ∈ l₂ ∨ x ∈+ l₂ α: Type u_1l: List αx: αl': List αhx✝: x ∈+ ll₁, l₂: List αy: αh: l₁ <+ l₂IH: x ∈+ l₁ → x ∈+ l₂hx: x ∈+ l₁cons₂.inry = x ∧ x ∈ l₂ ∨ x ∈+ l₂simp [IH: ?m.12137 l₁ l₂ hIH 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] <+ lduplicate_iff_sublist : x: αx ∈+ l: List αl ↔ [x: αx, x: αx] <+ l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx: αx ∈+ l ↔ [x, x] <+ linduction' l: List αl with y: ?m.13175y l: List ?m.13175l IH: ?m.13176 lIHα: Type u_1l: List αx: αnilx ∈+ [] ↔ [x, x] <+ []α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lconsx ∈+ y :: l ↔ [x, x] <+ y :: l
α: Type u_1l: List αx: αx ∈+ l ↔ [x, x] <+ l·α: Type u_1l: List αx: αnilx ∈+ [] ↔ [x, x] <+ [] α: Type u_1l: List αx: αnilx ∈+ [] ↔ [x, x] <+ []α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lconsx ∈+ y :: l ↔ [x, x] <+ y :: lsimpGoals accomplished! 🐙
α: Type u_1l: List αx: αx ∈+ l ↔ [x, x] <+ l·α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lconsx ∈+ y :: l ↔ [x, x] <+ y :: l α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lconsx ∈+ y :: l ↔ [x, x] <+ y :: lby_cases hx: ?m.13361hx : x: αx = y: ?m.13175yα: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: x = yposx ∈+ y :: l ↔ [x, x] <+ y :: lα: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: l
α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lconsx ∈+ y :: l ↔ [x, x] <+ y :: l·α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: x = yposx ∈+ y :: l ↔ [x, x] <+ y :: l α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: x = yposx ∈+ y :: l ↔ [x, x] <+ y :: lα: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: lsimp [hx: ?m.13354hx, 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 ∈ lsingleton_sublist]Goals accomplished! 🐙
α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lconsx ∈+ y :: l ↔ [x, x] <+ y :: l·α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: l α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: lrw [α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: lduplicate_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.13361hx,α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ l ↔ [x, x] <+ y :: l α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: lIH: ?m.13176 lIHα: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = yneg[x, x] <+ l ↔ [x, x] <+ y :: l]α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = yneg[x, x] <+ l ↔ [x, x] <+ y :: l
α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ 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.13175y, fun h: ?m.14245h => _: ?m.14230_⟩α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = yh: [x, x] <+ y :: lneg[x, x] <+ l
α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: lcases h: ?m.14245hα: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ya✝: [x, x] <+ lneg.cons[x, x] <+ lα: Type u_1l✝: List αx: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = xa✝: [x] <+ lneg.cons₂[x, x] <+ l
α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: l·α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ya✝: [x, x] <+ lneg.cons[x, x] <+ l α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ya✝: [x, x] <+ lneg.cons[x, x] <+ lα: Type u_1l✝: List αx: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = xa✝: [x] <+ lneg.cons₂[x, x] <+ lassumptionGoals accomplished! 🐙
α: Type u_1l✝: List αx, y: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = ynegx ∈+ y :: l ↔ [x, x] <+ y :: l·α: Type u_1l✝: List αx: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = xa✝: [x] <+ lneg.cons₂[x, x] <+ l α: Type u_1l✝: List αx: αl: List αIH: x ∈+ l ↔ [x, x] <+ lhx: ¬x = xa✝: [x] <+ lneg.cons₂[x, x] <+ lcontradictionGoals accomplished! 🐙
#align list.duplicate_iff_sublist List.duplicate_iff_sublist: ∀ {α : Type u_1} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ lList.duplicate_iff_sublist

theorem nodup_iff_forall_not_duplicate: Nodup l ↔ ∀ (x : α), ¬x ∈+ lnodup_iff_forall_not_duplicate : Nodup: {α : Type ?u.14605} → List α → PropNodup l: List αl ↔ ∀ x: αx : α: Type ?u.14597α, ¬x: αx ∈+ l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx: αNodup l ↔ ∀ (x : α), ¬x ∈+ lsimp_rw [α: Type u_1l: List αx: αNodup l ↔ ∀ (x : α), ¬x ∈+ lnodup_iff_sublist: ∀ {α : Type ?u.14658} {l : List α}, Nodup l ↔ ∀ (a : α), ¬[a, a] <+ lnodup_iff_sublist,α: Type u_1l: List αx: α(∀ (a : α), ¬[a, a] <+ l) ↔ ∀ (x : α), ¬x ∈+ l α: Type u_1l: List αx: αNodup l ↔ ∀ (x : α), ¬x ∈+ lduplicate_iff_sublist: ∀ {α : Type ?u.14754} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ lduplicate_iff_sublistGoals 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 ∈+ lList.nodup_iff_forall_not_duplicate

theorem exists_duplicate_iff_not_nodup: ∀ {α : Type u_1} {l : List α}, (∃ x, x ∈+ l) ↔ ¬Nodup lexists_duplicate_iff_not_nodup : (∃ x: αx : α: Type ?u.14847α, x: αx ∈+ l: List αl) ↔ ¬Nodup: {α : Type ?u.14864} → List α → PropNodup l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx: α(∃ x, x ∈+ l) ↔ ¬Nodup lsimp [nodup_iff_forall_not_duplicate: ∀ {α : Type ?u.14869} {l : List α}, Nodup l ↔ ∀ (x : α), ¬x ∈+ lnodup_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 lList.exists_duplicate_iff_not_nodup

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

theorem duplicate_iff_two_le_count: ∀ [inst : DecidableEq α], x ∈+ l ↔ 2 ≤ count x lduplicate_iff_two_le_count [DecidableEq: Sort ?u.16290 → Sort (max1?u.16290)DecidableEq α: Type ?u.16282α] : x: αx ∈+ l: List αl ↔ 2: ?m.163042 ≤ count: {α : Type ?u.16317} → [inst : BEq α] → α → List α → ℕcount x: αx l: List αl := byGoals accomplished! 🐙
α: Type u_1l: List αx: αinst✝: DecidableEq αx ∈+ l ↔ 2 ≤ count x lsimp [duplicate_iff_sublist: ∀ {α : Type ?u.16376} {l : List α} {x : α}, x ∈+ l ↔ [x, x] <+ lduplicate_iff_sublist, le_count_iff_replicate_sublist: ∀ {α : Type ?u.16394} {l : List α} [inst : DecidableEq α] {n : ℕ} {a : α}, n ≤ count a l ↔ replicate n a <+ lle_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 lList.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.17745List α: Type ?u.17725α, Decidable: Prop → TypeDecidable (x: αx ∈+ l: List αl)
| [] => isFalse: {p : Prop} → ¬p → Decidable pisFalse (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 pisTrue h: x ∈+ lh => isTrue: {p : Prop} → p → Decidable pisTrue (h: x ∈+ lh.duplicate_cons: ∀ {α : Type ?u.17844} {l : List α} {x : α}, x ∈+ l → ∀ (y : α), x ∈+ y :: lduplicate_cons y: αy)
| isFalse: {p : Prop} → ¬p → Decidable pisFalse h: ¬x ∈+ lh =>
if hx: ?m.17977hx : y: αy = x: αx ∧ x: αx ∈ l: List αl then isTrue: {p : Prop} → p → Decidable pisTrue (hx: ?m.17941hx.left: ∀ {a b : Prop}, a ∧ b → aleft.symm: ∀ {α : Sort ?u.17948} {a b : α}, a = b → b = asymm ▸ List.Mem.duplicate_cons_self: ∀ {α : Type ?u.17959} {l : List α} {x : α}, x ∈ l → x ∈+ x :: lList.Mem.duplicate_cons_self hx: ?m.17941hx.right: ∀ {a b : Prop}, a ∧ b → bright)
else isFalse: {p : Prop} → ¬p → Decidable pisFalse (byGoals accomplished! 🐙 α: Type ?u.17725l✝: List αx✝: αinst✝: DecidableEq αx, y: αl: List αh: ¬x ∈+ lhx: ¬(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 ∈+ lduplicate_cons_iff, h: ¬x ∈+ lh] using hx: ¬(y = x ∧ x ∈ l)hxGoals accomplished! 🐙)
#align list.decidable_duplicate List.decidableDuplicate: {α : Type u_1} → [inst : DecidableEq α] → (x : α) → (l : List α) → Decidable (x ∈+ l)List.decidableDuplicate

end List
```