How to prove ∃ x, a[i]? = some x

Stream: general

[Zihao Zhang]

import Mathlib

example {n:Nat}{a:List Char}(h1:n1 + 1 ≤ a.length):∃ x, a[a.length - (n1 + 1)]? = some x:=by
  sorry

[Zihao Zhang]

I think it is quite trivial, but I can't prove it.

[Sébastien Gouëzel]

import Mathlib

example {n1 : ℕ} {a : List Char} (h1 : n1 + 1 ≤ a.length) : ∃ x, a[a.length - (n1 + 1)]? = some x :=
  ⟨a[a.length - (n1 + 1)], by grind⟩

[Zihao Zhang]

Can I just use a theorem to prove this? I think there’s a direct one.

[Markus Himmel]

The closest is probably docs#getElem?_pos.