English
A recursion principle: to prove a property for all finite-length tuples, it suffices to prove it for the base case Fin.elim0 and to show that it is preserved under extending a tuple by cons at the head.
Русский
Принцип рекурсии: чтобы доказать свойство для всех кортежей конечной длины, достаточно доказать базовый случай Fin.elim0 и показать, что свойство сохраняется при добавлении элемента в голову через cons.
LaTeX
$$$\\text{consInduction}: \\forall \\alpha, \\text{motive},\\ \\motive\\text{ Fin.elim0} \\to (\\forall {n} {x_0} {x}, \\motive\\ x \\to \\motive(\\\\mathrm{Fin.cons} x_0 x)) \\to \\forall {n} (x: Fin n \\to \\alpha),\\ \\motive x$$$
Lean4
/-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple. -/
@[elab_as_elim]
def consCases {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x)) (x : ∀ i : Fin n.succ, α i) :
P x :=
_root_.cast (by rw [cons_self_tail]) <| h (x 0) (tail x)
