positivity on ∑ and ∑': works on the summand's syntax, not on ∀-hypotheses

Mathlib v4.35.0. positivity proves 0 ≤ ∑ n ∈ range 5, (f n)^2, 0 ≤ ∑' n, (f n)^2 and 0 ≤ ∑' n : ℕ, (1:ℝ)/((n:ℝ)+1)^2, because it recurses into the summand. It fails on 0 ≤ ∑ n ∈ range 5, f n even with h : ∀ n, 0 ≤ f n in context. Local hypotheses are only used for atoms, and a quantified one is never instantiated at the bound variable. In that case use Finset.sum_nonneg (fun i _ => h i) or tsum_nonneg h. The tsum lemma has an implicit SummationFilter argument L, so it only elaborates when there is an expected type. tsum_nonneg h as a bare linarith hint fails with 'don't know how to synthesize implicit argument L'. have : 0 ≤ ∑' n, f n := tsum_nonneg h works, and so does the inline ascription (tsum_nonneg h : 0 ≤ ∑' n, f n).