English
Let n be a natural number and α a family of types indexed by Fin n. For every m ≤ n, every v : (i : Fin n) → α i, every i : Fin m, and every x ∈ α (castLE h i), we have take m h (update v (castLE h i) x) = update (take m h v) i x.
Русский
Пусть n — натуральное число, α — семейство типов, индексируемое по Fin n. Для любого m ≤ n, для любого v : (i : Fin n) → α i, для любого i : Fin m и для любого x ∈ α (castLE h i) выполняется: take m h (update v (castLE h i) x) = update (take m h v) i x.
LaTeX
$$$\\forall n\\in\\mathbb{N}, \\forall \\alpha:\\mathrm{Fin}(n)\\to\\mathrm{Sort}, \\forall m\\le n, \\forall v:(i:\\mathrm{Fin}(n))\\to \\alpha(i), \\forall i:\\mathrm{Fin}(m), \\forall x\\in \\alpha(\\mathrm{castLE}\\,h\\,i): \\operatorname{take}(m,h)(\\operatorname{update} v(\\mathrm{castLE}\\,h\\,i)\\,x) = \\operatorname{update}(\\operatorname{take}(m,h)v)\\,i\\,x$$$
Lean4
/-- `take` commutes with `update` for indices in the range of `take`. -/
@[simp]
theorem take_update_of_lt (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) (x : α (castLE h i)) :
take m h (update v (castLE h i) x) = update (take m h v) i x :=
by
ext j
by_cases h' : j = i
· rw [h']
simp only [take, update_self]
· have : castLE h j ≠ castLE h i := by simp [h']
simp only [take, update_of_ne h', update_of_ne this]
