induction n with
| zero =>
    intro i h;
    simp;
| succ m ih =>
    intro i
    exact match i with
    | 0 => by simp [getF]
    | j+1 => by simp [rangeF, getF, ih]
n : ℕ
⊢ ∀ (i : ℕ) (h : i < length (rangeF n)), getF (rangeF n) i h = { val := i, isLt := (_ : i < n) }
no goals