case h
α : Type u
m n o : ℕ
m' : Type ?u.86190
n' : Type ?u.86193
o' : Type ?u.86196
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
α : Type u
m n o : ℕ
m' : Type ?u.86190
n' : Type ?u.86193
o' : Type ?u.86196
inst✝ : Neg α
x : α
v : Fin n → α
⊢ -vecCons x v = vecCons (-x) (-v)
ext i
no goals
case h
α : Type u
m n o : ℕ
m' : Type ?u.86190
n' : Type ?u.86193
o' : Type ?u.86196
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
refine' Fin.cases _ _ i <;> simp