case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x : α
h : Nodup []
⊢ [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x

case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
hl : Nodup tl → (tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x)
h : Nodup (hd :: tl)
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h : Nodup l
x : α
⊢ l ≠ [x] ↔ l = [] ∨ ∃ y, y ∈ l ∧ y ≠ x
induction' l with hd tl hl
no goals
case nil
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x : α
h : Nodup []
⊢ [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
simp
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
hl : Nodup tl → (tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x)
h : Nodup (hd :: tl)
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
specialize hl h.of_cons
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x

case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
case cons
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
by_cases hx : tl = [x]
no goals
case pos
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
simpa [hx, and_comm, and_or_left] using h
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : ¬tl = [x]
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
rw [← Ne.def, hl] at hx
case neg.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
h : Nodup [hd]
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x

case neg.inr.intro.intro
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
case neg
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
hx : tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
rcases hx with (rfl | ⟨y, hy, hx⟩)
no goals
case neg.inl
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
h : Nodup [hd]
hl : [] ≠ [x] ↔ [] = [] ∨ ∃ y, y ∈ [] ∧ y ≠ x
⊢ [hd] ≠ [x] ↔ [hd] = [] ∨ ∃ y, y ∈ [hd] ∧ y ≠ x
simp
case neg.inr.intro.intro
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ y x_1, y ≠ x
case neg.inr.intro.intro
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
suffices ∃ (y : α) (_ : y ∈ hd :: tl), y ≠ x by simpa [ne_nil_of_mem hy]
no goals
case neg.inr.intro.intro
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
⊢ ∃ y x_1, y ≠ x
exact ⟨y, mem_cons_of_mem _ hy, hx⟩
no goals
α : Type u
β : Type v
l✝ l₁ l₂ : List α
r : α → α → Prop
a b : α
l : List α
h✝ : Nodup l
x hd : α
tl : List α
h : Nodup (hd :: tl)
hl : tl ≠ [x] ↔ tl = [] ∨ ∃ y, y ∈ tl ∧ y ≠ x
y : α
hy : y ∈ tl
hx : y ≠ x
this : ∃ y x_1, y ≠ x
⊢ hd :: tl ≠ [x] ↔ hd :: tl = [] ∨ ∃ y, y ∈ hd :: tl ∧ y ≠ x
simpa [ne_nil_of_mem hy]