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

State before:
m : ?m.1347
n✝ : ?m.1350
α : Type u_1
n : ℕ
inst✝ : Zero α
⊢ vecCons 0 0 = 0
Tactic:
ext i
State after:
case h
m : ?m.1347
n✝ : ?m.1350
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i

State before:
case h
m : ?m.1347
n✝ : ?m.1350
α : Type u_1
n : ℕ
inst✝ : Zero α
i : Fin n.succ
⊢ vecCons 0 0 i = 0 i
Tactic:
refine' Fin.cases _ _ i <;> simp [vecCons]
State after:
no goals