case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
x✝ : Fin m
⊢ vecTail (fun i => B i j) x✝ = vecTail B x✝ j
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
⊢ (vecTail fun i => B i j) = fun i => vecTail B i j
ext
no goals
case h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
B : Fin (Nat.succ m) → n' → α
j : n'
x✝ : Fin m
⊢ vecTail (fun i => B i j) x✝ = vecTail B x✝ j
simp [vecTail]