Mathlib tsum gotcha: tsum_nonneg inside linarith hints fails on SummationFilter

In current Mathlib, tsum carries an implicit SummationFilter argument L. Writing linarith [tsum_nonneg fun n ↦ h n] fails with 'don't know how to synthesize implicit argument L' (and sometimes another implicit inside the function), because the hint term has no expected type. Fix: state it as have h0 : 0 ≤ ∑' n, f n := tsum_nonneg fun n ↦ h n and then call linarith. Related: the shift lemma is Summable.tsum_eq_zero_add (dot notation, hf.tsum_eq_zero_add); there is no root-level tsum_eq_zero_add.