[GOAL]
α : Type u_1
β : Type u_2
a : α
o : Option α
⊢ a ∈ toFinset o ↔ a ∈ o
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
a : α
⊢ a ∈ toFinset none ↔ a ∈ none
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case some
α : Type u_1
β : Type u_2
a val✝ : α
⊢ a ∈ toFinset (some val✝) ↔ a ∈ some val✝
[PROOFSTEP]
simp [eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
o : Option α
⊢ Finset.card (toFinset o) = Option.elim o 0 1
[PROOFSTEP]
cases o
[GOAL]
case none
α : Type u_1
β : Type u_2
⊢ Finset.card (toFinset none) = Option.elim none 0 1
[PROOFSTEP]
rfl
[GOAL]
case some
α : Type u_1
β : Type u_2
val✝ : α
⊢ Finset.card (toFinset (some val✝)) = Option.elim (some val✝) 0 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ ¬none ∈ map Embedding.some s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons none (map Embedding.some s) (_ : ¬none ∈ map Embedding.some s) ≤
      cons none (map Embedding.some t) (_ : ¬none ∈ map Embedding.some t) ↔
    s ≤ t
[PROOFSTEP]
rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
a : α
h : a ∈ none
⊢ a ∈ s
[PROOFSTEP]
cases h
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ (a_1 : α), a_1 ∈ some a → a_1 ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
a : α
⊢ some a ∈ ↑insertNone s ↔ a ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ card (↑insertNone s) = card s + 1
[PROOFSTEP]
simp [insertNone]
[GOAL]
α : Type u_1
β : Type u_2
s : Finset (Option α)
x : α
⊢ x ∈ ↑eraseNone s ↔ some x ∈ s
[PROOFSTEP]
simp [eraseNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ ↑eraseNone s = Finset.biUnion s Option.toFinset
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone s ↔ a✝ ∈ Finset.biUnion s Option.toFinset
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ ↑eraseNone (map Embedding.some s) = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
s : Finset α
a✝ : α
⊢ a✝ ∈ ↑eraseNone (map Embedding.some s) ↔ a✝ ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset α
⊢ ↑eraseNone (image some s) = s
[PROOFSTEP]
simpa only [map_eq_image] using eraseNone_map_some s
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ ↑eraseNone (s ∪ t) = ↑eraseNone s ∪ ↑eraseNone t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone (s ∪ t) ↔ a✝ ∈ ↑eraseNone s ∪ ↑eraseNone t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
⊢ ↑eraseNone (s ∩ t) = ↑eraseNone s ∩ ↑eraseNone t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq (Option α)
inst✝ : DecidableEq α
s t : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone (s ∩ t) ↔ a✝ ∈ ↑eraseNone s ∩ ↑eraseNone t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
⊢ ↑eraseNone ∅ = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
a✝ : α
⊢ a✝ ∈ ↑eraseNone ∅ ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
⊢ ↑eraseNone {none} = ∅
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
a✝ : α
⊢ a✝ ∈ ↑eraseNone {none} ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some (↑eraseNone s) = erase s none
[PROOFSTEP]
ext (_ | x)
[GOAL]
case a.none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ image some (↑eraseNone s) ↔ none ∈ erase s none
[PROOFSTEP]
simp
[GOAL]
case a.some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ image some (↑eraseNone s) ↔ some x ∈ erase s none
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ map Embedding.some (↑eraseNone s) = erase s none
[PROOFSTEP]
rw [map_eq_image, Embedding.some_apply, image_some_eraseNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ ↑insertNone (↑eraseNone s) = insert none s
[PROOFSTEP]
ext (_ | x)
[GOAL]
case a.none
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ none ∈ ↑insertNone (↑eraseNone s) ↔ none ∈ insert none s
[PROOFSTEP]
simp
[GOAL]
case a.some
α : Type u_1
β : Type u_2
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
x : α
⊢ some x ∈ ↑insertNone (↑eraseNone s) ↔ some x ∈ insert none s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s : Finset α
⊢ ↑eraseNone (↑insertNone s) = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
s : Finset α
a✝ : α
⊢ a✝ ∈ ↑eraseNone (↑insertNone s) ↔ a✝ ∈ s
[PROOFSTEP]
simp
