English
If you prepend an element x to u and append v, vecAppend ho (vecCons x u) v equals vecCons x (vecAppend (something) u v).
Русский
Если слева прибавить элемент x к векторu, а затем слева прибавить вектор с x к v, то vecAppend превращается в vecCons x (vecAppend …).
LaTeX
$$$\\operatorname{vecAppend}(ho,\\operatorname{vecCons}(x,u),v) = \\operatorname{vecCons}(x,\\operatorname{vecAppend}(\\text{by cutsat},u,v))$$$
Lean4
@[simp]
theorem cons_vecAppend (ho : o + 1 = m + 1 + n) (x : α) (u : Fin m → α) (v : Fin n → α) :
vecAppend ho (vecCons x u) v = vecCons x (vecAppend (by cutsat) u v) :=
by
ext i
simp_rw [vecAppend_eq_ite]
split_ifs with h
· rcases i with ⟨⟨⟩ | i, hi⟩
· simp
· simp only [Nat.add_lt_add_iff_right] at h
simp [h]
· rcases i with ⟨⟨⟩ | i, hi⟩
· simp at h
· rw [not_lt, Fin.val_mk, Nat.add_le_add_iff_right] at h
simp [not_lt.2 h]
