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