English
Let n be any natural, and for any m ≤ n and a function a : Fin n' → α, the first m·n' elements of Fin.repeat n a equal Fin.repeat m a.
Русский
Пусть n произвольно, и для любого m ≤ n и функции a : Fin n' → α первая часть длины m·n' от Fin.repeat n'a равна Fin.repeat m a.
LaTeX
$$$\\mathrm{take}(m \\cdot n')(\\mathrm{Nat}.\\mathrm{mul\\_le\\_mul\\_right}\, n'\\, h)\\; (\\mathrm{Fin}.\\mathrm{repeat}\\ n\\ a) = \\mathrm{Fin}.\\mathrm{repeat}\\ m\\ a$$
Lean4
theorem take_repeat {α : Type*} {n' : ℕ} (m : ℕ) (h : m ≤ n) (a : Fin n' → α) :
take (m * n') (Nat.mul_le_mul_right n' h) (Fin.repeat n a) = Fin.repeat m a :=
by
ext i
simp only [take, repeat_apply, modNat, coe_castLE]
