simp only [dom_iff, f_le_iff, f_apply, Subtype.coe_mk]
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ w1 n ≤ w
n✝ n : ℕ
inst✝ : NeZero n
w : Weight n 1
hw : w 0 = 0
⊢ ∀ (a : ↑(testvecs n 1)), E (w1 n) - pair (w1 n) ↑a ≤ E w - pair w ↑a