simp only [f_apply, E, ge_iff_le, pair'_v]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(f w a) = pair' w (v a) / (↑n + 1) + 1
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
h : (↑n + 1) * ↑(pair w ↑a) ≤ ↑d * ↑(Weight.sum w)
H : pair w ↑a ≤ Weight.sum w * d / (n + 1) + 1
⊢ ↑(Weight.sum w * d / (n + 1) + 1 - pair w ↑a) = (↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)) / (↑n + 1) + 1