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.