feat: port `cc` tactic (3/3)

[Komyyy]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/cc.20tactic.20comes.20to.20Lean4

---

• [x] depends on: #11960

[digama0]

Note: I have pushed an update to the lean toolchain because this PR was on a buggy version of the toolchain. WARNING: checking out old commits of this PR using v4.2.0-rc2 or v4.2.0-rc3 can cause lake clean to delete your mathlib folder! If you need to do so, make sure to delete lakefile.olean manually before running any lake commands.

[Komyyy]

@Vierkantor

I'm very happy that this tactic is being ported! However, I find it difficult to start reviewing the PR (my browser can barely open the diff). Would you be able to split it up into several smaller pull requests so we can get this moving?

I've splitted it up now. Sorry for the long absence of updates.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11960~~ By Dependent Issues (🤖). Happy coding!

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style