case h
α : Type u
m n o : ℕ
m' : Type ?u.58053
n' : Type ?u.58056
o' : Type ?u.58059
inst✝ : Add α
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.58053
n' : Type ?u.58056
o' : Type ?u.58059
inst✝ : Add α
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.58053
n' : Type ?u.58056
o' : Type ?u.58059
inst✝ : Add α
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]