feat: the terminal refine linter

[adomani]

A linter that warns on usages of refine and refine' as a finishing tactic.

See this Zulip discussion.

Conclusion of the experiment

Systematic replacements of terminal refine with exact leads to an overall slow-down.

---

[adomani]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5f02e63.
There were significant changes against commit e545009:

  Benchmark                                                Metric         Change
  ==============================================================================
+ build                                                    linting         -5.2%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties   instructions    -4.2%

[adomani]

Here are the benchmark results for commit 5f02e63. There were significant changes against commit e545009:

  Benchmark                                                Metric         Change
  ==============================================================================
+ build                                                    linting         -5.2%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties   instructions    -4.2%

Do not be fooled by the green: the PR is largely a slowdown!