case a
α : Type u_1
β : Type ?u.18177
s : Finset α
a✝ : α
⊢ a✝ ∈ ↑eraseNone (↑insertNone s) ↔ a✝ ∈ s
α : Type u_1
β : Type ?u.18177
s : Finset α
⊢ ↑eraseNone (↑insertNone s) = s
ext
no goals
case a
α : Type u_1
β : Type ?u.18177
s : Finset α
a✝ : α
⊢ a✝ ∈ ↑eraseNone (↑insertNone s) ↔ a✝ ∈ s
simp