@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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