if h : i < (ofFn f).length then
  rw [get?_eq_get h]
  rw [length_ofFn] at h
  rw [dif_pos h]
  simp
else
  rw [get?_eq_none.mpr (by simpa using h)]
  rw [length_ofFn] at h
  rw [dif_neg h]
  rfl
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
no goals