simp only [← nsmul_eq_mul]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ i in range (n + 1), ↑(Nat.choose n i) * f i ≤ ↑(2 ^ n) * B
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → ℝ
B : ℝ
h : ∀ i ∈ range (n + 1), f i ≤ B
⊢ ∑ x in range (n + 1), Nat.choose n x • f x ≤ 2 ^ n • B