@[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)

def Fin.appendCases {α : Sort u_2} {m n : ℕ} {motive : (Fin (m + n) → α) → Sort u_1} (append : (f : Fin m → α) → (g : Fin n → α) → motive (append f g)) (x : Fin (m + n) → α) : motive x

Equations

• Fin.appendCases append x = cast ⋯ (append (fun (i : Fin m) => x (Fin.castAdd n i)) fun (i : Fin n) => x (Fin.natAdd m i))