English
A property P holds for all i in Fin(n+1) iff it holds for the last element and for all i in Fin n, P(i.castSucc).
Русский
Свойство P выполняется для всех индексов Fin(n+1) тогда и только тогда, когда оно выполняется для последнего элемента и для всех i в Fin n, P(i.castSucc).
LaTeX
$$$Iff (\\\\forall i, P i) (\\\\land \\\\; P (\\\\mathrm{last} \\\\; n) \\\\land \\\\; \\\\forall i : Fin n, P i.castSucc)$$$
Lean4
theorem append_cons {α : Sort*} (a : α) (as : Fin n → α) (bs : Fin m → α) :
Fin.append (cons a as) bs = cons a (Fin.append as bs) ∘ (Fin.cast <| Nat.add_right_comm n 1 m) :=
by
funext i
rcases i with ⟨i, -⟩
simp only [append, addCases, cons, castLT, comp_apply]
rcases i with - | i
· simp
· split_ifs with h
· have : i < n := Nat.lt_of_succ_lt_succ h
simp [addCases, this]
· have : ¬i < n := Nat.not_le.mpr <| Nat.lt_succ.mp <| Nat.not_le.mp h
simp [addCases, this]
