case a
α : Type u_1
β : Type ?u.8977
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone s ↔ a✝ ∈ Finset.biUnion s Option.toFinset
α : Type u_1
β : Type ?u.8977
inst✝ : DecidableEq α
s : Finset (Option α)
⊢ ↑eraseNone s = Finset.biUnion s Option.toFinset
ext
no goals
case a
α : Type u_1
β : Type ?u.8977
inst✝ : DecidableEq α
s : Finset (Option α)
a✝ : α
⊢ a✝ ∈ ↑eraseNone s ↔ a✝ ∈ Finset.biUnion s Option.toFinset
simp