no goals
ι : Type ?u.507203
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
inst✝ : Inhabited α
l : List α
x : α
xs : List α
n✝ n : ℕ
⊢ getI l n = Option.iget (get? l n)
rw [← getD_default_eq_getI, getD_eq_getD_get?, Option.getD_default_eq_iget]