English
consCases is a recursion principle that, given a way to handle a cons-head, reduces any (n+1)-tuple to the head and tail case.
Русский
ConsCases — рекурсивный принцип, который, имея способ обработки головы cons, сводит любой (n+1)-кортеж к случаю головы и хвоста.
LaTeX
$$$\\text{consCases} : \\{P : ((i : Fin n.succ) \\to \\alpha i) \\to \\text{Sort}\\ v\\} \\to (\\forall x0 x, P(\\\\mathrm{Fin.cons} x0 x)) \\to (x : (i : Fin n.succ) \\to \\alpha i) \\to P x$$$
Lean4
/-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.cons`. -/
@[elab_as_elim]
def consInduction {α : Sort*} {motive : ∀ {n : ℕ}, (Fin n → α) → Sort v} (elim0 : motive Fin.elim0)
(cons : ∀ {n} (x₀) (x : Fin n → α), motive x → motive (Fin.cons x₀ x)) : ∀ {n : ℕ} (x : Fin n → α), motive x
| 0, x => by convert elim0
| _ + 1, x => consCases (fun _ _ ↦ cons _ _ <| consInduction elim0 cons _) x
