split_ifs with h
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
⊢ 1 ≤ E w - pair w ↑a + if a = tw n 1 0 then 0 else 1
case pos
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 0

case neg
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
a : ↑(testvecs n 1)
h : ¬a = tw n 1 0
⊢ 1 ≤ E w - pair w ↑a + 1