English
For any predicate P on Fin(n+1), Exists i, P i is equivalent to (Exists i : Fin n, P i.castSucc) or 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}\\}, \\Exists i, P i \\iff (\\Exists i : \\mathrm{Fin} n, P i.castSucc) \\lor P(\\mathrm{Fin.last}\\, n). $$$$
Lean4
theorem exists_fin_succ' {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ (∃ i : Fin n, P i.castSucc) ∨ P (.last _) :=
⟨fun ⟨i, h⟩ => Fin.lastCases Or.inr (fun i hi => Or.inl ⟨i, hi⟩) i h, fun h =>
h.elim (fun ⟨i, hi⟩ => ⟨i.castSucc, hi⟩) (fun h => ⟨.last _, h⟩)⟩
