[GOAL]
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
[PROOFSTEP]
induction' h with l' _ y l' _ hm
[GOAL]
case cons_mem
α : Type u_1
l : List α
x : α
l' : List α
a✝ : x ∈ l'
⊢ x ∈ x :: l'
[PROOFSTEP]
exact mem_cons_self _ _
[GOAL]
case cons_duplicate
α : Type u_1
l : List α
x y : α
l' : List α
a✝ : x ∈+ l'
hm : x ∈ l'
⊢ x ∈ y :: l'
[PROOFSTEP]
exact mem_cons_of_mem _ hm
[GOAL]
α : Type u_1
l : List α
x : α
h : x ∈+ x :: l
⊢ x ∈ l
[PROOFSTEP]
cases' h with _ h _ _ h
[GOAL]
case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l
[PROOFSTEP]
exact h
[GOAL]
case cons_duplicate
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l
[PROOFSTEP]
exact h.mem
[GOAL]
α : Type u_1
l : List α
x : α
h : x ∈+ l
y : α
⊢ l ≠ [y]
[PROOFSTEP]
induction' h with l' h z l' h _
[GOAL]
case cons_mem
α : Type u_1
l : List α
x y : α
l' : List α
h : x ∈ l'
⊢ x :: l' ≠ [y]
[PROOFSTEP]
simp [ne_nil_of_mem h]
[GOAL]
case cons_duplicate
α : Type u_1
l : List α
x y z : α
l' : List α
h : x ∈+ l'
a_ih✝ : l' ≠ [y]
⊢ z :: l' ≠ [y]
[PROOFSTEP]
simp [ne_nil_of_mem h.mem]
[GOAL]
α : Type u_1
l : List α
x y : α
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
cases' h with _ hm _ _ hm
[GOAL]
case refine'_1.cons_mem
α : Type u_1
l : List α
x : α
hm : x ∈ l
⊢ x = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
exact Or.inl ⟨rfl, hm⟩
[GOAL]
case refine'_1.cons_duplicate
α : Type u_1
l : List α
x y : α
hm : x ∈+ l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l
[PROOFSTEP]
exact Or.inr hm
[GOAL]
case refine'_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l
[PROOFSTEP]
rcases h with (⟨rfl | h⟩ | h)
[GOAL]
case refine'_2.inl.intro.refl
α : Type u_1
l : List α
x : α
right✝ : x ∈ l
⊢ x ∈+ x :: l
[PROOFSTEP]
simpa
[GOAL]
case refine'_2.inr
α : Type u_1
l : List α
x y : α
h : x ∈+ l
⊢ x ∈+ y :: l
[PROOFSTEP]
exact h.cons_duplicate
[GOAL]
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l
[PROOFSTEP]
simpa [duplicate_cons_iff, hx.symm] using h
[GOAL]
α : Type u_1
l : List α
x y : α
hne : x ≠ y
⊢ x ∈+ y :: l ↔ x ∈+ l
[PROOFSTEP]
simp [duplicate_cons_iff, hne.symm]
[GOAL]
α : Type u_1
l : List α
x : α
l' : List α
hx : x ∈+ l
h : l <+ l'
⊢ x ∈+ l'
[PROOFSTEP]
induction' h with l₁ l₂ y _ IH l₁ l₂ y h IH
[GOAL]
case slnil
α : Type u_1
l : List α
x : α
l' : List α
hx✝ : x ∈+ l
hx : x ∈+ []
⊢ x ∈+ []
[PROOFSTEP]
exact hx
[GOAL]
case cons
α : 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₁
⊢ x ∈+ y :: l₂
[PROOFSTEP]
exact (IH hx).duplicate_cons _
[GOAL]
case cons₂
α : 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₁
⊢ x ∈+ y :: l₂
[PROOFSTEP]
rw [duplicate_cons_iff] at hx ⊢
[GOAL]
case cons₂
α : 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₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
[PROOFSTEP]
rcases hx with (⟨rfl, hx⟩ | hx)
[GOAL]
case cons₂.inl.intro
α : Type u_1
l l' l₁ l₂ : List α
y : α
h : l₁ <+ l₂
hx✝ : y ∈+ l
IH : y ∈+ l₁ → y ∈+ l₂
hx : y ∈ l₁
⊢ y = y ∧ y ∈ l₂ ∨ y ∈+ l₂
[PROOFSTEP]
simp [h.subset hx]
[GOAL]
case cons₂.inr
α : 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₁
⊢ y = x ∧ x ∈ l₂ ∨ x ∈+ l₂
[PROOFSTEP]
simp [IH hx]
[GOAL]
α : Type u_1
l : List α
x : α
⊢ x ∈+ l ↔ [x, x] <+ l
[PROOFSTEP]
induction' l with y l IH
[GOAL]
case nil
α : Type u_1
l : List α
x : α
⊢ x ∈+ [] ↔ [x, x] <+ []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
[PROOFSTEP]
by_cases hx : x = y
[GOAL]
case pos
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
[PROOFSTEP]
simp [hx, cons_sublist_cons_iff, singleton_sublist]
[GOAL]
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ x ∈+ y :: l ↔ [x, x] <+ y :: l
[PROOFSTEP]
rw [duplicate_cons_iff_of_ne hx, IH]
[GOAL]
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
⊢ [x, x] <+ l ↔ [x, x] <+ y :: l
[PROOFSTEP]
refine' ⟨sublist_cons_of_sublist y, fun h => _⟩
[GOAL]
case neg
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
h : [x, x] <+ y :: l
⊢ [x, x] <+ l
[PROOFSTEP]
cases h
[GOAL]
case neg.cons
α : Type u_1
l✝ : List α
x y : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = y
a✝ : [x, x] <+ l
⊢ [x, x] <+ l
[PROOFSTEP]
assumption
[GOAL]
case neg.cons₂
α : Type u_1
l✝ : List α
x : α
l : List α
IH : x ∈+ l ↔ [x, x] <+ l
hx : ¬x = x
a✝ : [x] <+ l
⊢ [x, x] <+ l
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
l : List α
x : α
⊢ Nodup l ↔ ∀ (x : α), ¬x ∈+ l
[PROOFSTEP]
simp_rw [nodup_iff_sublist, duplicate_iff_sublist]
[GOAL]
α : Type u_1
l : List α
x : α
⊢ (∃ x, x ∈+ l) ↔ ¬Nodup l
[PROOFSTEP]
simp [nodup_iff_forall_not_duplicate]
[GOAL]
α : Type u_1
l : List α
x : α
inst✝ : DecidableEq α
⊢ x ∈+ l ↔ 2 ≤ count x l
[PROOFSTEP]
simp [duplicate_iff_sublist, le_count_iff_replicate_sublist]
[GOAL]
α : Type u_1
l✝ : List α
x✝ : α
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x ∈+ l
hx : ¬(y = x ∧ x ∈ l)
⊢ ¬x ∈+ y :: l
[PROOFSTEP]
simpa [duplicate_cons_iff, h] using hx
