English
List.take m h (List.ofFn v) equals the function take m h v under a cast, i.e., the get at position i matches.
Русский
List.take m h (List.ofFn v) сопоставимо с взятием m элементов через v с приводами, т.е. элемент на позиции i совпадает.
LaTeX
$$$((\\operatorname{List.ofFn} v).\\operatorname{take} m)\\\\.\\text{get} = \\operatorname{take}(m,h)\\,v \\circ \\mathrm{Fin.cast}(\\mathrm{List.length\\_take\\_of\\_le}\\,h)$$$
Lean4
/-- Alternative version of `take_eq_take_list_ofFn` with `l : List α` instead of `v : Fin n → α`. -/
theorem ofFn_take_get {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) : List.ofFn (take m h l.get) = l.take m :=
List.ext_get (by simp [h]) (fun n h1 h2 => by simp)
