feat: symmetric monoidal structure on graded objects

[joelriou]

---

(Refactor of #6379) This is a draft. It shall be split in separate PR later:

• [ ] depends on: #14457
• [ ] depends on: #14343
• [x] depends on: #7425
• [x] depends on: #8237
• [x] depends on: #8239
• [x] depends on: #8242
• [x] depends on: #10667
• [x] depends on: #10700
• [x] depends on: #10701
• [x] depends on: #10747
• [x] depends on: #11676
• [x] depends on: #11687
• [x] depends on: #11701
• [x] depends on: #11703
• [x] depends on: #14339

[github-actions[bot]]

PR summary c4d8f2b94c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.GradedObject.Braiding	552

---

Declarations diff

+ braidedCategory + braiding + braiding_naturality_left + braiding_naturality_right + hexagon_forward + hexagon_reverse + on + symmetricCategory + symmetry

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.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#14457~~
• ~~leanprover-community/mathlib4#14343~~
• ~~leanprover-community/mathlib4#7425~~
• ~~leanprover-community/mathlib4#8237~~
• ~~leanprover-community/mathlib4#8239~~
• ~~leanprover-community/mathlib4#8242~~
• ~~leanprover-community/mathlib4#10667~~
• ~~leanprover-community/mathlib4#10700~~
• ~~leanprover-community/mathlib4#10701~~
• ~~leanprover-community/mathlib4#10747~~
• ~~leanprover-community/mathlib4#11676~~
• ~~leanprover-community/mathlib4#11687~~
• ~~leanprover-community/mathlib4#11701~~
• ~~leanprover-community/mathlib4#11703~~
• ~~leanprover-community/mathlib4#14339~~ By Dependent Issues (🤖). Happy coding!

[jcommelin]

@joelriou Is this still WIP?

[joelriou]

@joelriou Is this still WIP?

Indeed, it is now ready for review.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style