English
The inverse of the bijection induced by castSucc, when applied to an element i of Fin(n+1) lying in the image of castSucc, returns the original natural value of i.
Русский
Обратное к биекции, порожденной castSucc, примененное к элементу i ∈ Fin(n+1) из образа castSucc, возвращает исходное натуральное значение i.
LaTeX
$$$$ \\forall n \\in \\mathbb{N}, \\forall i \\in \\mathrm{Fin}(n+1), \\text{if } i \\in \\operatorname{range}(\\operatorname{castSucc}) \\text{ then } ((\\operatorname{Equiv.ofInjective}(\\operatorname{castSucc})^{-1}) i) = i. $$$$
Lean4
@[simp]
theorem coe_of_injective_castSucc_symm {n : ℕ} (i : Fin n.succ) (hi) :
((Equiv.ofInjective castSucc (castSucc_injective _)).symm ⟨i, hi⟩ : ℕ) = i :=
by
rw [← coe_castSucc]
exact congr_arg val (Equiv.apply_ofInjective_symm _ _)
