rw [get?_eq_get h]
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ ((ofFn f).get? i).getD d = if h : i < k then f ⟨i, h⟩ else d
k : Nat
α : Type u_1
i : Nat
d : α
f : Fin k → α
h : i < (ofFn f).length
⊢ (some ((ofFn f).get ⟨i, h⟩)).getD d = if h : i < k then f ⟨i, h⟩ else d