The doc at https://leanprover-community.github.io/extras/simp.html says about sync:

all it does is repeatedly replace (or rewrite) subterms of the form A by B, for all applicable facts of the form A = B or A ↔ B. The simplifier mindlessly rewrites until it can rewrite no more.

This raises some questions as to how this works in practice:

• Does simp only perform a brute force search or is it smarter?
• How does simp never end in a cyclic behavior?
• Is there some limit in the number of steps it takes to try to obtain the target?

The doc at https://leanprover-community.github.io/extras/simp.html says about simp:

all it does is repeatedly replace (or rewrite) subterms of the form A by B, for all applicable facts of the form A = B or A ↔ B. The simplifier mindlessly rewrites until it can rewrite no more.

This raises some questions as to how this works in practice:

• Does simp only perform a brute force search or is it smarter?
• How does simp never end in a cyclic behavior?
• Is there some limit in the number of steps it takes to try to obtain the target?