chore(Data/Finsupp/Order): add Finsupp.support_add_eq' for canonically ordered Finsupps

[Yu-Misaka]

Greetings! This PR attempts to show that in a CanonicallyOrderedAdd setting, the support of f1 + f2 is exactly the union of the supports of f1 and f2. This result will be handy in combinatorics and when the coefficients are in natural number (for example here)

---

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary a48f3f9d84

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ support_add_eq_union

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit a48f3f9d84
Reference commit 97f12126be

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Copilot]

Pull request overview

Note

Copilot was unable to run its full agentic suite in this review.

Adds a lemma characterizing Finsupp.support of an addition as the union of supports, in the canonically-ordered setting used by this file.

Changes:

• Introduces support_add_eq', proving support (f1 + f2) = support f1 ∪ support f2.
• Uses support_mono plus le_self_add/le_add_self to prove the reverse inclusion.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[faenuccio]

Thanks for the PR! I'm having a look, but please consider that although this PR is quite short, we only add the easy label for much shorter things, that are probably completely uncontroversial. In this case, one might wonder if the variables are correct, if the file is the right one, if the style is OK... (I'm not saying that they are not, just that this PR is above what we call "easy").

[faenuccio]

Why do you need a prime?

[Yu-Misaka]

Beacuse we have a Finsupp.support_add_eq that takes disjoint support set (although I do believe this needs a better name, will support_add_eq_union suggested by copilot sounds better?)

[Yu-Misaka]

Thanks for the PR! I'm having a look, but please consider that although this PR is quite short, we only add the easy label for much shorter things, that are probably completely uncontroversial. In this case, one might wonder if the variables are correct, if the file is the right one, if the style is OK... (I'm not saying that they are not, just that this PR is above what we call "easy").

Ah! I see, thanks for pointing this out!

[faenuccio]

Beacuse we have a Finsupp.support_add_eq that takes disjoint support set (although I do believe this needs a better name, will support_add_eq_union suggested by copilot sounds better?)

Ah sure, good point. Can you then please add a small doc both to this and to support_add_eq, mutually pointing to one another and saying " in the case... there is also..."?

[Yu-Misaka]

Beacuse we have a Finsupp.support_add_eq that takes disjoint support set (although I do believe this needs a better name, will support_add_eq_union suggested by copilot sounds better?)

Ah sure, good point. Can you then please add a small doc both to this and to support_add_eq, mutually pointing to one another and saying " in the case... there is also..."?

Sure! Does it look better now?