English
If n ≤ k, then the range of Fin.castLE h is the set of i ∈ Fin k with i.val < n.
Русский
Если n ≤ k, то образ Fin.castLE h равен множеству i ∈ Fin k с i.val < n.
LaTeX
$$$\\forall n,k \\in \\mathbb{N},\\ (n \\le k) \\Rightarrow \\mathrm{Set.range}(\\mathrm{Fin.castLE}\\ h) = \\{ i \\in \\mathrm{Fin}(k) \\mid i.\\mathrm{val} < n \\}$$$
Lean4
/-- The `Fin.succ_one_eq_two` in `Lean` only applies in `Fin (n+2)`.
This one instead uses a `NeZero n` typeclass hypothesis.
-/
@[simp]
theorem succ_one_eq_two' [NeZero n] : Fin.succ (1 : Fin (n + 1)) = 2 :=
by
cases n
· exact (NeZero.ne 0 rfl).elim
·
rfl
-- Version of `succ_one_eq_two` to be used by `dsimp`.
-- Note the `'` swapped around due to a move to std4.
