ENNReal.sum_geometric_two_pow_toNNReal

lemma ENNReal.sum_geometric_two_pow_toNNReal {k : ℕ} (hk : k > 0) :    ∑' (n : ℕ), (2 : ℝ≥0∞) ^ (-k * n : ℤ) = (1 / (1 - 1 / 2 ^ k) : ℝ).toNNReal := by  conv_lhs =>    enter [1, n]    rw [← rpow_intCast, show (-k * n : ℤ) = (-k * n : ℝ) by simp, rpow_mul, rpow_natCast]  rw [tsum_geometric, show (2 : ℝ≥0∞) = (2 : ℝ).toNNReal by simp,    ← coe_rpow_of_ne_zero (by simp), ← Real.toNNReal_rpow_of_nonneg zero_le_two,    ← coe_one, ← Real.toNNReal_one, ← coe_sub, NNReal.sub_def,    Real.toNNReal_one, NNReal.coe_one, Real.coe_toNNReal', max_eq_left (by positivity),    Real.rpow_neg zero_le_two, Real.rpow_natCast, one_div]  have : ((1 : ℝ) - (2 ^ k)⁻¹).toNNReal ≠ 0 := by    rw [ne_eq, Real.toNNReal_eq_zero, tsub_le_iff_right, zero_add, not_le, inv_lt_one_iff₀]    right; exact one_lt_pow₀ (M₀ := ℝ) _root_.one_lt_two hk.ne'  rw [← coe_inv this, coe_inj, Real.toNNReal_inv, one_div]