feat(Tactic/Linter): add unicode linter for unicode variant-selectors

[joneugster]

Unicode characters can be followed by one of the two "variant-selectors" \FE0E (text) or \FE0F (emoji).
These appear to the user as a single unicode character and they might copy them by accident. For example ✅️ (\u2705\uFE0F), ✅ (\u2705) and ✅︎ (\u2705\uFE0E) are three variants of the "same" unicode character. The one without variant-selector might display as either emoji or not, depending on the user's device and font.

Add unicode linter ensuring variant-selector only appear on specified characters and also ensuring these characters always have the correct variant selector to avoid confusions.

Everything flagged by this linter can be fixed fully automatically with lake exe lint-style --fix or by commenting bot fix style on the PR.

---

This is the first PR of a series of PRs about unicode characters in Mathlib. The second PR will be addressing non-breaking spaces.

• part 2: feat(Tactic/Linter): add unicode linter for unwanted characters #17131 (mostly independent to this PR)
• part 3: feat(Tactic/Linter): lint unwanted unicode #16215

Zulip discussions:

• https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Whitelist.20for.20Unicode.3F
• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20specific.20font
• private reviewer stream: "request for speedy review"

Generally, the discussions seemed to show favour for the first two PRs in this series (handling variant selectors & dealing with invisible chars. such as   (\u00A0)) while there seems to be still room for discussion about what to do with general unicode characters (whitelist, blacklist, ...)

Related PRs:

• RFC: Use emoji variant selector for unicode characters leanprover/lean4#5015 added some emoji-variant selectors to Emojis used in Lean itself.

[github-actions]

PR summary b9c6d10e3a

Import changes exceeding 2%

%	File
+5.00%	Mathlib.Tactic.Linter.TextBased

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Tactic.Linter.TextBased Mathlib.Tactic	1
Mathlib.Tactic.Linter.UnicodeLinter (new file)	18

---

Declarations diff

+ UnicodeVariant.emoji
+ UnicodeVariant.text
+ emojis
+ findBadUnicode
+ findBadUnicodeAux
+ nonEmojis
+ printCodepointHex
+ removeQuotations
+ unicodeLinter

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[joneugster]

bot fix style