[Merged by Bors] - feat(Tactic/Positivity): cover Finset.sum_pos' with the Finset.sum extension - #43613

[Merged by Bors] - feat(Tactic/Positivity): cover Finset.sum_pos' with the Finset.sum extension#43613

YaelDillies wants to merge 8 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

YaelDillies:positivity_finset_sum_posYaelDillies/mathlib4:positivity_finset_sum_posCopy head branch name to clipboard