case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ col (vecCons x u) i j = vecCons (fun x_1 => x) (col u) i j
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
⊢ col (vecCons x u) = vecCons (fun x_1 => x) (col u)
ext (i j)
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i : Fin (Nat.succ m)
j : Unit
⊢ col (vecCons x u) i j = vecCons (fun x_1 => x) (col u) i j
refine' Fin.cases _ _ i <;> simp [vecHead, vecTail]