no goals
ι : Type ?u.93582
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ get? l (indexOf a l) = some a
rw [nthLe_get?, indexOf_nthLe (indexOf_lt_length.2 h)]