no goals
ι : Type ?u.369711
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
l : List (Option α)
x : α
⊢ (∃ i, get? l i = some (some x)) ↔ ∃ i, get? (reduceOption l) i = some x
rw [← mem_iff_get?, ← mem_iff_get?, reduceOption_mem_iff]