English
A standard associativity-like rule: append (cons a as) bs equals cons a (append as bs) under the appropriate cast.
Русский
Стандартное свойство ассоциативности: append (cons a as) bs равняется cons a (append as bs) с учётом приведения.
LaTeX
$$$\\\\operatorname{append}(\\\\operatorname{cons} a \\\\; as) bs = \\\\operatorname{cons} a (\\\\operatorname{append} as bs) \\\\circ \\\\operatorname{cast} (\\\\mathrm{Nat.add\_right\_comm} n 1 m)$$$
Lean4
theorem append_snoc {α : Sort*} (as : Fin n → α) (bs : Fin m → α) (b : α) :
Fin.append as (snoc bs b) = snoc (Fin.append as bs) b :=
by
funext i
rcases i with ⟨i, isLt⟩
simp only [append, addCases, castLT, cast_mk, subNat_mk, natAdd_mk, cast, snoc.eq_1, eq_rec_constant, Nat.add_eq,
castLT_mk]
split_ifs with lt_n lt_add sub_lt nlt_add lt_add <;> (try rfl)
· have := Nat.lt_add_right m lt_n
contradiction
· obtain rfl := Nat.eq_of_le_of_lt_succ (Nat.not_lt.mp nlt_add) isLt
simp [Nat.add_comm n m] at sub_lt
· have := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp lt_n) lt_add
contradiction
