English
snocCases applied to a snoc yields the expected value: snocCases h (snoc x x0) = h x x0.
Русский
snocCases, применяемый к snoc, даёт ожидаемое значение: snocCases h (snoc x x0) = h x x0.
LaTeX
$$$\\\\operatorname{snocCases} h (\\\\operatorname{snoc} x x_0) = h x x_0$$$
Lean4
/-- Equivalence between tuples of length `n + 1` and pairs of an element and a tuple of length `n`
given by separating out the last element of the tuple.
This is `Fin.snoc` as an `Equiv`. -/
@[simps]
def snocEquiv (α : Fin (n + 1) → Type*) : α (last n) × (∀ i, α (castSucc i)) ≃ ∀ i, α i
where
toFun f _ := Fin.snoc f.2 f.1 _
invFun f := ⟨f _, Fin.init f⟩
left_inv f := by simp
right_inv f := by simp
