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

State before:
m : ?m.4819
n✝ : ?m.4822
α : Type u_1
n : ℕ
inst✝² : Zero α
inst✝¹ : SMulZeroClass ℝ α
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
⊢ vecCons x v + vecCons y w = vecCons (x + y) (v + w)
Tactic:
ext i
State after:
case h
m : ?m.4819
n✝ : ?m.4822
α : Type u_1
n : ℕ
inst✝² : Zero α
inst✝¹ : SMulZeroClass ℝ α
inst✝ : Add α
x : α
v : Fin n → α
y : α
w : Fin n → α
i : Fin n.succ
⊢ (vecCons x v + vecCons y w) i = vecCons (x + y) (v + w) i

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