f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤ ↔ (∑' (b : ℕ), ↑(f b)) = ⊤
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f
simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Ne.def, not_iff_not, ENNReal.coe_mul,
  ENNReal.coe_pow, ENNReal.coe_two]
case mp
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h : (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
⊢ (∑' (b : ℕ), ↑(f b)) = ⊤

case mpr
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h : (∑' (b : ℕ), ↑(f b)) = ⊤
⊢ (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤ ↔ (∑' (b : ℕ), ↑(f b)) = ⊤
constructor <;> intro h
case mp
f : ℕ → ℝ≥0
h : (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ (∑' (b : ℕ), ↑(f b)) = ⊤
case mp
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h : (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
⊢ (∑' (b : ℕ), ↑(f b)) = ⊤
replace hf : ∀ m n, 1 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
  ENNReal.coe_le_coe.2 (hf (zero_lt_one.trans hm) hmn)
no goals
case mp
f : ℕ → ℝ≥0
h : (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
hf : ∀ (m n : ℕ), 1 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ (∑' (b : ℕ), ↑(f b)) = ⊤
simpa [h, ENNReal.add_eq_top, ENNReal.mul_eq_top] using ENNReal.tsum_condensed_le hf
case mpr
f : ℕ → ℝ≥0
h : (∑' (b : ℕ), ↑(f b)) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
case mpr
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h : (∑' (b : ℕ), ↑(f b)) = ⊤
⊢ (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
replace hf : ∀ m n, 0 < m → m ≤ n → (f n : ℝ≥0∞) ≤ f m := fun m n hm hmn =>
  ENNReal.coe_le_coe.2 (hf hm hmn)
no goals
case mpr
f : ℕ → ℝ≥0
h : (∑' (b : ℕ), ↑(f b)) = ⊤
hf : ∀ (m n : ℕ), 0 < m → m ≤ n → ↑(f n) ≤ ↑(f m)
⊢ (∑' (b : ℕ), 2 ^ b * ↑(f (2 ^ b))) = ⊤
simpa [h, ENNReal.add_eq_top] using ENNReal.le_tsum_condensed hf