English
If the left part is exhausted, i.e., a.size ≤ i, then (a ++ b).extract i j = b.extract (i - a.size) (j - a.size).
Русский
Если левая часть исчерпана, то (a ++ b).extract i j = b.extract (i - a.size) (j - a.size).
LaTeX
$$$(a\;++\;b).extract\;i\;j = b.extract\; (i - a.size)\; (j - a.size) \quad (a.size \le i)$$$
Lean4
/-- This is a stronger version of `Array.extract_append_right`,
and should be upstreamed to replace that.
-/
theorem extract_append_right' {a b : Array α} {i j : Nat} (h : a.size ≤ i) :
(a ++ b).extract i j = b.extract (i - a.size) (j - a.size) :=
by
apply ext
· rw [size_extract, size_extract, size_append]
omega
· intro k hi h2
rw [getElem_extract, getElem_extract, getElem_append_right (by cutsat)]
congr
cutsat
