[Merged by Bors] - feat: toAdditive to transfer MatcherInfo data

[nomeata]

so that printing the definitions shows match … with properly, and
meta code looking for matchers work.

Fixes an item on #1074

[github-actions]

PR summary c1a5e8e4dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

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

[grunweg]

Thanks for fixing this! I guess/hope that a few workarounds for this issue can be removed now (search for #1074, item (8)). Would you like to perform this clean-up also?

[nomeata]

Would you like to perform this clean-up also?

I wouldn’t mind if someone else will do that :-)

[grunweg]

Never mind, this actually fixes item 7 on the list: I don't see any obvious locations where this would simplify mathlib code.

[nomeata]

This is also needed after leanprover/lean4#4154 hits lean master, so if we merge it now then the nightly testing maintainers (@semorrison and @jcommelin) have less work with the next nightly.

[kim-em]

Sold!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style