English
The function predAbove is injective on Fin n (as a function from Fin(n+1) to Fin n).
Русский
Функция predAbove инъективна на Fin(n+1) → Fin(n).
LaTeX
$$$\text{Injective}(\mathrm{predAbove} : \mathrm{Fin}(n+1) \to \mathrm{Fin}(n))$$$
Lean4
/-- `predAbove` is injective at the pivot -/
theorem predAbove_left_injective : Injective (@predAbove n) :=
by
intro i j hij
obtain ⟨n, rfl⟩ := Nat.exists_add_one_eq.2 i.size_positive
wlog h : i < j generalizing i j
· simp only [not_lt] at h
obtain h | rfl := h.lt_or_eq
· exact (this hij.symm h).symm
· rfl
replace hij := congr_fun hij i.succ
rw [predAbove_succ_self, Fin.predAbove_of_le_castSucc _ _ (by simpa), ← Fin.castSucc_inj, castSucc_castPred] at hij
exact (i.castSucc_lt_succ.ne hij).elim
