[Merged by Bors] - port the clean tactic from lean 3 to lean 4

[mkaratarakis]

---

[kmill]

I'd suggest that once #5717 is merged that we put this tactic in the DefeqTransformations file and use the runDefeqTactic function to run it, like the other tactics there. That means you don't have to reinvent how to run an expression-transformation tactic, and you get clean at h and clean at * for free.

[kmill]

Ah, I really misunderstood what this tactic was about. Now I understand that clean t is like exact t but removes type hints from t, so my suggestion to use the defeq transformations framework doesn't make sense.

@digama0 You write the original version of clean. It looks like it was only ever used in a single place in mathlib -- is it still useful? Should we turn it into a cleanHints% term elaborator instead? That way you can write stuff like let x := cleanHints% by ... or exact cleanHints% by .... Or maybe it could be a classical-like tactic that takes a tactic sequence instead of a term?

[digama0]

I think it would make sense as a term elaborator.

[PatrickMassot]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style