English
Let P be a predicate on Fin(n+1). For any p in Fin(n+1), the following holds: the existence of some i with P(i) is equivalent to P(p) or the existence of some i with P(p.succAbove(i)).
Русский
Пусть P — предикат на Fin(n+1). Пусть p ∈ Fin(n+1). Тогда верно: существует i с P(i) тогда и только тогда, когда P(p) или существует i, такое что P(p.succAbove(i)).
LaTeX
$$$\exists i: \mathrm{Fin}(n+1), P(i) \\iff P(p) \lor \exists i: \mathrm{Fin} n, P(p.\\succAbove i).$$$
Lean4
theorem exists_iff_succAbove {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) : (∃ i, P i) ↔ P p ∨ ∃ i, P (p.succAbove i)
where
mp := by
rintro ⟨i, hi⟩
induction i using p.succAboveCases
· exact .inl hi
· exact .inr ⟨_, hi⟩
mpr := by rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩
