have h' : ∀ k, k ≠ j → a.val k = 0
case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a
case h'
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
⊢ ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0

case h
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
⊢ { val := Function.update 0 j 1, property := (_ : (fun x => x ∈ testvecs n 1) (Function.update 0 j 1)) } = a