English
Taking the first m elements of addCases u v is the same as taking the first m elements of u, provided m ≤ n.
Русский
Взятие первых m элементов из addCases u v равно взятию первых m элементов из u при условии m ≤ n.
LaTeX
$$$\\forall {n,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}(m,\\mathrm{Nat.le_add_right_of_le}\\,h)\\bigl(\\mathrm{Fin.addCases}\\,u\\,v\\bigr) = \\operatorname{take}(m,h) u$$$
Lean4
/-- Taking the first `m ≤ n` elements of an `addCases u v`, where `u` is a `n`-tuple, is the same as
taking the first `m` elements of `u`. -/
theorem take_addCases_left {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 m (Nat.le_add_right_of_le h) (addCases u v) = take m h u :=
by
ext i
have : i < n := Nat.lt_of_lt_of_le i.isLt h
simp only [take, addCases, this, coe_castLE, ↓reduceDIte]
congr
