[Merged by Bors] - chore(Mathlib/Tactic/ToAdditive/Frontend): isolate the to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend (2/2)

[Komyyy]

Ideally, we want to move the attribute [to_additive] commands in Init.ZeroOne into Tactic.ToAdditive without any other changes.
However, the to_additive attribute is initialized in the file and cannot be included in the same file.
So it would be necessary to isolate the original to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend, and create an new file Tactic.ToAdditive as a placeholder for the attribute [to_additive] commands in Init.ZeroOne.
But if we put these two changes in the same PR, git cannot recognizes that Tactic.ToAdditive is renamed, so we split the PR.

---

• depends on: [Merged by Bors] - chore(Mathlib/Tactic/ToAdditive/Frontend): isolate the to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend (1/2) #14816

[github-actions]

PR summary 11a78505f3

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Too many changes (4290)!

---

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>

[jcommelin]

Dear @Komyyy I still don't understand why the file Tactic/ToAdditive needs to be renamed in the same PR that touches Mathlib/Init/ZeroOne. I would like to have a PR that does only the changes to Tactic/ToAdditive.

[Komyyy]

@jcommelin
Ideally, the attribute [to_additive] commands in Init.ZeroOne should be moved into Tactic.ToAdditive without any other changes.
However, the to_additive attribute is initialized in the file and cannot be included in the same file. So I thought it would be necessary to isolate the original to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend in the same PR as the PR to which the commands in Init.ZeroOne are moved.

[jcommelin]

I think you can do the "isolation" part before moving the commands in Init.ZeroOne. Or am I missing something?

[Komyyy]

@jcommelin
I made this PR do only isolation part and moved the part moving the commands in Init.ZeroOne to #14642.

[jcommelin]

Thanks. This is now an atomic change.
I assume it will pass CI, but let's wait to be sure:

bors d+

[mathlib-bors]

✌️ Komyyy can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Komyyy]

bors r+

[Komyyy]

bors r-

[mathlib-bors]

Canceled.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Mathlib/Tactic/ToAdditive/Frontend): isolate the to_additive attribute implementation in a new file Tactic.ToAdditive.Frontend (1/2) #14816
  By Dependent Issues (🤖). Happy coding!

[YaelDillies]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style