no goals
α : Type u_1
β : Type ?u.2246
s : Finset α
a : α
h : a ∈ none
⊢ a ∈ s
cases h
no goals
α : Type u_1
β : Type ?u.2246
s : Finset α
a : α
⊢ some a = none ∨ some a ∈ (map Embedding.some s).val ↔ ∀ (a_1 : α), a_1 ∈ some a → a_1 ∈ s
simp