case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (n + 1), 2 ^ k • f (2 ^ k) = f 1 + 2 • ∑ k in range n, 2 ^ k • f (2 ^ (k + 1))
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (n + 1), 2 ^ k • f (2 ^ k) ≤ f 1 + 2 • ∑ k in Ico 2 (2 ^ n + 1), f k
convert add_le_add_left (nsmul_le_nsmul_of_le_right (sum_condensed_le' hf n) 2) (f 1)
no goals
case h.e'_3
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ ∑ k in range (n + 1), 2 ^ k • f (2 ^ k) = f 1 + 2 • ∑ k in range n, 2 ^ k • f (2 ^ (k + 1))
simp [sum_range_succ', add_comm, pow_succ, mul_nsmul', sum_nsmul]