English
If a ∈ s, then there exists n and s' with some (a, s') in destruct (drop s n).
Русский
Если a ∈ s, то существует n и s', где some (a, s') встречается в destruct (drop s n).
LaTeX
$$$$\forall s:\\mathrm{WSeq}\,\alpha,\forall a:\\alpha,\ a \in s \Rightarrow \exists n\exists s',\text{some }(a,s') \in \mathrm{destruct}(\mathrm{drop}\,s\,n).$$$$
Lean4
theorem exists_get?_of_mem {s : WSeq α} {a} (h : a ∈ s) : ∃ n, some a ∈ get? s n :=
by
apply mem_rec_on h
· intro a' s' h
rcases h with h | h
· exists 0
simp only [get?, drop, head_cons]
rw [h]
apply ret_mem
· obtain ⟨n, h⟩ := h
exists n + 1
simpa [get?]
· intro s' h
obtain ⟨n, h⟩ := h
exists n
simp only [get?, dropn_think, head_think]
apply think_mem h
