English
Taking the first n+m elements of addCases u v equals addCases u (take m h v).
Русский
Взятие первых n+m элементов из addCases u v равно addCases u (take m h v).
LaTeX
$$$\\forall {n'}\\ (m:\\mathbb{N})\\ (h:\\ m \\le n')\\ (u:(i:\\mathrm{Fin}(n))\\to \\mathrm{motive}(\\mathrm{Fin.castAdd}\\,n'\\,i))\\ (v:(i:\\mathrm{Fin}(n'))\\to \\mathrm{motive}(\\mathrm{Fin.natAdd}\\,n\\,i)):\\ \\operatorname{take}(\\mathrm{instHAdd.hAdd}\\,n\\,m)\\bigl(\\mathrm{Fin.addCases}\\,u\\,v\\bigr) = \\mathrm{Fin.addCases}\\,u\\bigl(\\operatorname{take} m h v\\bigr)$$$
Lean4
/-- Taking the first `n + m` elements of an `addCases u v`, where `v` is a `n'`-tuple and `m ≤ n'`,
is the same as appending `u` with the first `m` elements of `v`. -/
theorem take_addCases_right {n' : ℕ} {motive : Fin (n + n') → Sort*} (m : ℕ) (h : m ≤ n')
(u : (i : Fin n) → motive (castAdd n' i)) (v : (i : Fin n') → motive (natAdd n i)) :
take (n + m) (Nat.add_le_add_left h n) (addCases u v) = addCases u (take m h v) :=
by
ext i
simp only [take, addCases, coe_castLE]
by_cases h' : i < n
· simp only [h', ↓reduceDIte]
congr
· simp only [h', ↓reduceDIte, subNat, castLE, Fin.cast, eqRec_eq_cast]
