[Merged by Bors] - feat(Data/Finsupp): add lemmas for Finsupp and Sum

[BryceT233]

This PR adds various computational lemmas related to operations of finitely supported functions. Alongside #35329, theses lemmas provide the necessary helpers to construct various equivalences for MvPowerSeries.

---

[github-actions]

PR summary 08fd1302b1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ comapDomain_inl_sumElim
+ comapDomain_inr_sumElim
+ comapDomain_sumElim_comapDomain
+ embDomain_inl
+ embDomain_inr
+ image_sumElim_product_antidiagonal
+ optionElim_add
+ sumElim_add

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./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).

[Vierkantor]

A few remarks but overall this looks useful, thanks for covering this area! 🎉

[BryceT233]

Thanks for the review! I applied the suggestions, but currently the lint style check fails due to some windows line endings issues and I am trying to fix it.

[BryceT233]

It looks like an auto-fix script ran and somehow rewrote the entire file when I was testing.

[BryceT233]

I tried reverting my changes to Basic.lean and Option.lean, but GitHub is still showing them as modified in the diff. Additionally, the lint error regarding windows line endings (CRLF) is still persisting. I'd really appreciate some guidance on how to get these issues resolved! Maybe I should reopen the PR? Thanks!

[BryceT233]

-awaiting-author

[Vierkantor]

Glad to see that you managed to figure out the accidental changes, sadly I was busy with other work and couldn't take a look at it until now.

Thank you for the PR!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Build