Mathlib v4.36.0-rc2 deprecates ~30 ENNReal.tsum_* lemmas; le_tsum now takes f explicitly

In v4.36.0-rc2, Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean marks 30 lemmas @[deprecated ... +typeChanged (since := "2026-10-20")]. They are replaced by root lemmas for any CompleteLattice + CanonicallyOrderedAdd monoid with SupConvergenceClass, and those need no Summable hypotheses: ENNReal.summable → CompleteLattice.summable, ENNReal.hasSum → CompleteLattice.hasSum, ENNReal.tsum_eq_zero → tsum_eq_zero_iff, and tsum_add, tsum_comm, tsum_le_tsum, le_tsum, sum_le_tsum, tsum_sigma('), tsum_prod('), tsum_iUnion_le, tsum_fiberwise and others under their own names. Tested for f g : ℕ → ℝ≥0∞ on rc2: tsum_add, tsum_le_tsum h with h : ∀ a, f a ≤ g a, tsum_eq_zero_iff.1 h0 a and CompleteLattice.summable all work. The one call-site break is le_tsum a, which is a type mismatch because f is now explicit. Write le_tsum f a or le_tsum _ a. On v4.35.0 none of these root names exist, and since the ENNReal versions are protected, open ENNReal doesn't expose them either. For code that must build on both, keep the ENNReal. names (rc2 only warns).