Theorem: Matrix.smul_vecCons (CvxLean/Lib/Math/Data/Matrix.lean)

State before:
m : ?m.2988
n✝ : ?m.2991
α : Type u_1
n : ℕ
inst✝¹ : Zero α
inst✝ : SMulZeroClass ℝ α
x : ℝ
y : α
v : Fin n → α
⊢ x • vecCons y v = vecCons (x • y) (x • v)
Tactic:
ext i
State after:
case h
m : ?m.2988
n✝ : ?m.2991
α : Type u_1
n : ℕ
inst✝¹ : Zero α
inst✝ : SMulZeroClass ℝ α
x : ℝ
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i

State before:
case h
m : ?m.2988
n✝ : ?m.2991
α : Type u_1
n : ℕ
inst✝¹ : Zero α
inst✝ : SMulZeroClass ℝ α
x : ℝ
y : α
v : Fin n → α
i : Fin n.succ
⊢ (x • vecCons y v) i = vecCons (x • y) (x • v) i
Tactic:
refine' Fin.cases _ _ i <;> simp [vecCons]
State after:
no goals