cc

Stream: new members

[Alex Zhang]

I know that the tactic cc stands for congruence closure. But I don't quite understand what congruence closure means and what kinds of goals it can solve. Could anyone please give some explanations?

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/tactics.html#cc%20(congruence%20closure)