no goals
n i : Nat
H : i < length (range n)
⊢ some (get (range n) { val := i, isLt := H }) = some i
rw [← get?_eq_get _, get?_range (by simpa using H)]
no goals
n i : Nat
H : i < length (range n)
⊢ i < n
simpa using H