case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), x ∈ s → False

case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ (x : α), x ∈ s → x ∈ xs
induction' xs with xs_hd generalizing s <;> simp [*, Finset.enum]
no goals
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ s : Finset α
⊢ s = ∅ ↔ ∀ (x : α), x ∈ s → False
simp [Finset.eq_empty_iff_forall_not_mem]
case cons.mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝

case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) ↔ ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
constructor
case cons.mp.intro.intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
h' : s = a ∨ s = {xs_hd} ∪ a
x : α
hx : x ∈ s
⊢ x = xs_hd ∨ x ∈ tail✝
case cons.mp
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)) → ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
rintro ⟨a, h, h'⟩ x hx
case cons.mp.intro.intro.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x = xs_hd ∨ x ∈ tail✝

case cons.mp.intro.intro.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h' : s = {xs_hd} ∪ a
⊢ x = xs_hd ∨ x ∈ tail✝
case cons.mp.intro.intro
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
h' : s = a ∨ s = {xs_hd} ∪ a
x : α
hx : x ∈ s
⊢ x = xs_hd ∨ x ∈ tail✝
cases' h' with _ h' a b
case cons.mp.intro.intro.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x ∈ tail✝
case cons.mp.intro.intro.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x = xs_hd ∨ x ∈ tail✝
right
case cons.mp.intro.intro.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x ∈ a
case cons.mp.intro.intro.inl.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x ∈ tail✝
apply h
case cons.mp.intro.intro.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
x : α
hx : x ∈ s
h : ∀ (x : α), x ∈ s → x ∈ tail✝
⊢ x ∈ s
case cons.mp.intro.intro.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h✝ : s = a
⊢ x ∈ a
subst a
no goals
case cons.mp.intro.intro.inl.h.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
x : α
hx : x ∈ s
h : ∀ (x : α), x ∈ s → x ∈ tail✝
⊢ x ∈ s
exact hx
case cons.mp.intro.intro.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx : x = xs_hd ∨ x ∈ a
⊢ x = xs_hd ∨ x ∈ tail✝
case cons.mp.intro.intro.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
hx : x ∈ s
h' : s = {xs_hd} ∪ a
⊢ x = xs_hd ∨ x ∈ tail✝
simp only [h', mem_union, mem_singleton] at hx⊢
case cons.mp.intro.intro.inr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx : x = xs_hd
⊢ x = xs_hd ∨ x ∈ tail✝

case cons.mp.intro.intro.inr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx' : x ∈ a
⊢ x = xs_hd ∨ x ∈ tail✝
case cons.mp.intro.intro.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx : x = xs_hd ∨ x ∈ a
⊢ x = xs_hd ∨ x ∈ tail✝
cases' hx with hx hx'
no goals
case cons.mp.intro.intro.inr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx : x = xs_hd
⊢ x = xs_hd ∨ x ∈ tail✝
exact Or.inl hx
no goals
case cons.mp.intro.intro.inr.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s a : Finset α
h : ∀ (x : α), x ∈ a → x ∈ tail✝
x : α
h' : s = {xs_hd} ∪ a
hx' : x ∈ a
⊢ x = xs_hd ∨ x ∈ tail✝
exact Or.inr (h _ hx')
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
⊢ (∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝) → ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
intro h
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ (∀ (x : α), x ∈ s \ {xs_hd} → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ ∃ a, (∀ (x : α), x ∈ a → x ∈ tail✝) ∧ (s = a ∨ s = {xs_hd} ∪ a)
exists s \ ({xs_hd} : Finset α)
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ (∀ (x : α), x ∈ s \ {xs_hd} → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
simp only [and_imp, mem_sdiff, mem_singleton]
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → x = xs_hd ∨ x ∈ tail✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
simp only [or_iff_not_imp_left] at h
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
⊢ (∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝) ∧ (s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd})
exists h
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
case cons.mpr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
by_cases h : xs_hd ∈ s
case this
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
⊢ {xs_hd} ⊆ s

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
this : {xs_hd} ⊆ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
have : {xs_hd} ⊆ s
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
this : {xs_hd} ⊆ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
case this
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
⊢ {xs_hd} ⊆ s

case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
this : {xs_hd} ⊆ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
simp only [HasSubset.Subset, *, forall_eq, mem_singleton]
no goals
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : xs_hd ∈ s
this : {xs_hd} ⊆ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
simp only [union_sdiff_of_subset this, or_true_iff, Finset.union_sdiff_of_subset,
  eq_self_iff_true]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd}
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd} ∨ s = {xs_hd} ∪ s \ {xs_hd}
left
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s \ {xs_hd} = s
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s = s \ {xs_hd}
symm
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s ∩ {xs_hd} ⊆ ∅
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s \ {xs_hd} = s
simp only [sdiff_eq_self]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s ∩ {xs_hd} → a ∈ ∅
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
⊢ s ∩ {xs_hd} ⊆ ∅
intro a
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s → a = xs_hd → a ∈ ∅
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s ∩ {xs_hd} → a ∈ ∅
simp only [and_imp, mem_inter, mem_singleton]
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
a : α
h₀ : a ∈ s
h✝ : ∀ (x : α), x ∈ s → ¬x = a → x ∈ tail✝
h : ¬a ∈ s
⊢ a ∈ ∅
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
xs_hd : α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
h✝ : ∀ (x : α), x ∈ s → ¬x = xs_hd → x ∈ tail✝
h : ¬xs_hd ∈ s
a : α
⊢ a ∈ s → a = xs_hd → a ∈ ∅
rintro h₀ rfl
no goals
case neg.h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s✝ : Finset α
tail✝ : List α
tail_ih✝ : ∀ (s : Finset α), s ∈ enum tail✝ ↔ ∀ (x : α), x ∈ s → x ∈ tail✝
s : Finset α
a : α
h₀ : a ∈ s
h✝ : ∀ (x : α), x ∈ s → ¬x = a → x ∈ tail✝
h : ¬a ∈ s
⊢ a ∈ ∅
exact (h h₀).elim