[Merged by Bors] - chore: replace many refine' with refine

[adomani]

This PR replaces 7979 refine' with refine. Many of the left-over ones cannot actually be directly replaced by refine <add some ?>.

Zulip thread

---

[adomani]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6beb1d0.Found no runs to compare against.

[kbuzzard]

!Stoll-bench @MichaelStollBayreuth

[github-actions]

No declarations were harmed in the making of this PR! 🐙

---

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[adomani]

Benchmark using master from a couple of commits ago (thanks Matt!).

[MichaelStollBayreuth]

Unfortunately, http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/7154f447-eacb-45e1-b172-599fa45c4fa8?all_values=true does not work here (which is how my script gets the json file with the information). If someone knowns the right incantation for this case, I can produce a more detailed summary.

[adomani]

@MichaelStollBayreuth, Matt provided a better bench that I linked shortly before you posted your comment: does that benchmark help?

[MichaelStollBayreuth]

@adomani That's the one I was trying.

[adomani]

Oh, sorry, I clicked on the link and I could see nothing.

[mattrobball]

Ok, I removed the lines starting with whitespace, an optional dot, optional whitespace, and then refine. This left about 2k lines of the diff. I went through those ?_ by ?_ to make sure nothing was off.

bors merge p=90001

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style