case h
α : Type u
m n o : ℕ
m' : Type ?u.54537
n' : Type ?u.54540
o' : Type ?u.54543
M : Type u_1
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
α : Type u
m n o : ℕ
m' : Type ?u.54537
n' : Type ?u.54540
o' : Type ?u.54543
M : Type u_1
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)
ext i
no goals
case h
α : Type u
m n o : ℕ
m' : Type ?u.54537
n' : Type ?u.54540
o' : Type ?u.54543
M : Type u_1
inst✝ : SMul M α
x : M
y : α
v : Fin n → α
i : Fin (Nat.succ n)
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
refine' Fin.cases _ _ i <;> simp