no goals
ι : Type ?u.369416
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
x : α
⊢ x ∈ reduceOption l ↔ some x ∈ l
simp only [reduceOption, id.def, mem_filterMap, exists_eq_right]