-- Mathlib/Data/List/Nodup.lean
theorem Nodup.ne_singleton_iff {l : List α} (h : Nodup l) (x : α) :
    l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x

Proof state:
case pos
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
simpa [hx, and_comm, and_or_left] using h

Result:
no goals

Proof state:
case nil
α : Type u
x : α
h : [].Nodup
⊢ [] ≠ [x] ↔ [] = [] ∨ ∃ y ∈ [], y ≠ x

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
x hd : α
tl : List α
hl : tl.Nodup → (tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x)
h : (hd :: tl).Nodup
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
specialize hl h.of_cons

Result:
case cons
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Proof state:
case neg
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
rw [← Ne, hl] at hx

Result:
case neg
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
hx : tl = [] ∨ ∃ y ∈ tl, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Proof state:
case neg.inr.intro.intro
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
suffices ∃ y ∈ hd :: tl, y ≠ x by simpa [ne_nil_of_mem hy]

Result:
case neg.inr.intro.intro
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ y ∈ hd :: tl, y ≠ x

Proof state:
case neg
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
hx : tl = [] ∨ ∃ y ∈ tl, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
rcases hx with (rfl | ⟨y, hy, hx⟩)

Result:
case neg.inl
α : Type u
x hd : α
h : [hd].Nodup
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y ∈ [], y ≠ x
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y ∈ [hd], y ≠ x

case neg.inr.intro.intro
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Proof state:
case neg.inl
α : Type u
x hd : α
h : [hd].Nodup
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y ∈ [], y ≠ x
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y ∈ [hd], y ≠ x

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
by_cases hx : tl = [x]

Result:
case pos
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

case neg
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Proof state:
case neg.inr.intro.intro
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
exact ⟨y, mem_cons_of_mem _ hy, hx⟩

Result:
no goals

Proof state:
α : Type u
x hd : α
tl : List α
h : (hd :: tl).Nodup
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
this : ∃ y ∈ hd :: tl, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x

Tactic:
simpa [ne_nil_of_mem hy]

Result:
no goals

Proof state:
α : Type u
l : List α
h : l.Nodup
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u
x : α
h : [].Nodup
⊢ [] ≠ [x] ↔ [] = [] ∨ ∃ y ∈ [], y ≠ x

case cons
α : Type u
x hd : α
tl : List α
hl : tl.Nodup → (tl ≠ [x] ↔ tl = [] ∨ ∃ y ∈ tl, y ≠ x)
h : (hd :: tl).Nodup
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y ∈ hd :: tl, y ≠ x