English
For any predicate P on Fin(n+1), (for all i in Fin(n+1), P i) is equivalent to (for all i in Fin n, P i.castSucc) and P(last n).
Русский
Для любого предиката P на Fin(n+1): (для всех i, P i) эквивалентно (для всех i в Fin n, P i.castSucc) и P(last n).
LaTeX
$$$$ \\forall {n : \\mathbb{N}} \\{P : \\mathrm{Fin}(n+1) \\to \\mathrm{Prop}\\}, \\ (\\forall i, P i) \\iff (\\forall i : \\mathrm{Fin} n, P i.castSucc) \\land P(\\mathrm{Fin.last}\\, n). $$$$
Lean4
theorem forall_fin_succ' {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ (∀ i : Fin n, P i.castSucc) ∧ P (.last _) :=
⟨fun H => ⟨fun _ => H _, H _⟩, fun ⟨H0, H1⟩ i => Fin.lastCases H1 H0 i⟩
-- to match `Fin.eq_zero_or_eq_succ`
