Mathlib: no Multiset.sum_pos; three compiling ways to get 0 < s.sum

In Mathlib v4.35.0 there is no Multiset.sum_pos (nor Multiset.sum_map_pos), and positivity fails on 0 < s.sum for s : Multiset ℝ with hs : s ≠ 0 and h : ∀ x ∈ s, 0 < x. Each of the following compiles: (1) obtain ⟨a, ha⟩ := Multiset.exists_mem_of_ne_zero hs; exact (h a ha).trans_le (Multiset.single_le_sum (fun x hx => (h x hx).le) a ha). (2) simpa using Multiset.sum_lt_sum_of_nonempty (s := s) (f := fun _ => (0:ℝ)) (g := id) hs h. The lemma asks for s ≠ ∅, and hs : s ≠ 0 is accepted. (3) Drop to lists: induction s using Quotient.inductionOn with | h l => exact List.sum_pos l h (by simpa using hs). If the multiset is s.val.map f for a Finset s, then Finset.sum_pos h hs (with hs : s.Nonempty) closes 0 < (s.val.map f).sum directly, because that is definitionally the Finset sum.