Appending tuples

Lemmas about Fin.append not (yet) in Mathlib: the two parts of an appended tuple never overlap and appending commutes with post-composition and with updating an entry on either side.

theorem Fin.castAdd_ne_natAdd {m n : ℕ} (i : Fin m) (j : Fin n) : castAdd n i ≠ natAdd m j

The two parts of Fin.append never overlap.

theorem Fin.comp_append {α : Sort u_1} {β : Sort u_2} {m n : ℕ} (f : α → β) (a : Fin m → α) (b : Fin n → α) : f ∘ append a b = append (f ∘ a) (f ∘ b)

Post-composition commutes with Fin.append.

theorem Fin.append_update_left {α : Sort u_1} {m n : ℕ} (a : Fin m → α) (b : Fin n → α) (i : Fin m) (x : α) : append (Function.update a i x) b = Function.update (append a b) (castAdd n i) x

Updating an entry of the left tuple is updating the appended tuple at castAdd.

theorem Fin.append_update_right {α : Sort u_1} {m n : ℕ} (a : Fin m → α) (b : Fin n → α) (i : Fin n) (x : α) : append a (Function.update b i x) = Function.update (append a b) (natAdd m i) x

Updating an entry of the right tuple is updating the appended tuple at natAdd.