Lean4
/-- The congruence closure tactic `cc` tries to solve the goal by chaining
equalities from context and applying congruence (i.e. if `a = b`, then `f a = f b`).
It is a finishing tactic, i.e. it is meant to close
the current goal, not to make some inconclusive progress.
A mostly trivial example would be:
```lean
example (a b c : ℕ) (f : ℕ → ℕ) (h : a = b) (h' : b = c) : f a = f c := by
cc
```
As an example requiring some thinking to do by hand, consider:
```lean
example (f : ℕ → ℕ) (x : ℕ)
(H1 : f (f (f x)) = x) (H2 : f (f (f (f (f x)))) = x) :
f x = x := by
cc
``` -/
@[tactic_parser 1000]
public meta def _root_.Mathlib.Tactic.cc : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.CC._root_.Mathlib.Tactic.cc 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "cc" false✝) Lean.Parser.Tactic.optConfig)
