case h
α : Type u
m n o : ℕ
m' : Type ?u.66213
n' : Type ?u.66216
o' : Type ?u.66219
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
α : Type u
m n o : ℕ
m' : Type ?u.66213
n' : Type ?u.66216
o' : Type ?u.66219
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
⊢ vecCons x v - w = vecCons (x - vecHead w) (v - vecTail w)
ext i
no goals
case h
α : Type u
m n o : ℕ
m' : Type ?u.66213
n' : Type ?u.66216
o' : Type ?u.66219
inst✝ : Sub α
x : α
v : Fin n → α
w : Fin (Nat.succ n) → α
i : Fin (Nat.succ n)
⊢ (vecCons x v - w) i = vecCons (x - vecHead w) (v - vecTail w) i
refine' Fin.cases _ _ i <;> simp [vecHead, vecTail]