Bounding a tsum explicitly in Lean: sum_le_hasSum with hasSum_zeta_two and geometric

To turn a summability proof into a numeric bound on ∑' n, f n (f ≥ 0), prove a uniform bound on the partial sums and finish with Real.tsum_le_of_sum_range_le hf h. For the partial sums, sum_le_hasSum (range M) (fun i _ ↦ by positivity) hasSum_zeta_two gives ∑_{n<M+1} 1/n² ≤ π²/6. The n = 0 term is 1/0 = 0, so rewrite with sum_range_succ' to shift to 1/(k+1)². Similarly, (hasSum_geometric_of_lt_one hr0 hr1).mul_left r handles ∑ r^{k+1} ≤ r/(1-r). For the numerics, Real.pi_lt_d4 (π < 3.1416) and Real.log_two_gt_d9 work. Bound r = 2^{-1/5} by contradiction: r^5 = 1/2 via ← Real.rpow_natCast, ← Real.rpow_mul, then gcongr on t ↦ t^5. norm_num closes the final rational inequality.