English
If m < n and s.get? m = some x, then x is an element of s.take n.
Русский
Если m < n и s.get? m = some x, то x принадлежит s.take n.
LaTeX
$$$m < n \Rightarrow s.get? m = \mathrm{some}(x) \Rightarrow x \in \mathrm{take}(n, s)$$$
Lean4
theorem get?_mem_take {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α} (h_get : s.get? m = some x) : x ∈ s.take n := by
induction m generalizing n s with
| zero =>
obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
rw [← hl, take, head_eq_some h_get]
simp
| succ k ih =>
obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_lt h_mn
subst hl
have : ∃ y, s.get? 0 = some y := by
apply ge_stable _ _ h_get
simp
obtain ⟨y, hy⟩ := this
rw [take, head_eq_some hy]
simp
right
apply ih (by cutsat)
rwa [get?_tail]
