Commit 2024-06-23 23:52 bff23e15
View on Github →chore: restore cc tactic (#13404)
The cc tactic is a high-cost tactic, so I restored cc tactics only if a proof can be reduced significantly.
I made sure that cc tactic works on in the all changed proofs except when the other specification changes in Lean 4 changes a goal.