have h₁ : ∃ j, 0 < a.val j
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, ↑a j = 1
case h₁
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
⊢ ∃ j, 0 < ↑a j

case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
h₁ : ∃ j, 0 < ↑a j
⊢ ∃ j, ↑a j = 1