refactor: remove the last use of Lean.(HashSet|HashMap)

[hargoniX]

No description provided.

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit a3fb005.
There were significant changes against commit 5eea835:

  Benchmark            Metric                 Change
  =============================================================
+ import Lean          task-clock              -8.2%  (-22.8 σ)
+ import Lean          wall-clock              -8.2%  (-23.7 σ)
- lake build no-op     maxrss                   1.6%  (121.3 σ)
- lake config elab     maxrss                   2.2% (1893.3 σ)
- lake config import   instructions             1.2%   (70.6 σ)
- lake config import   maxrss                   2.3%  (233.5 σ)
- lake config tree     instructions             1.2%   (17.5 σ)
- lake config tree     maxrss                   2.3%  (233.3 σ)
- lake env             instructions             1.3%   (27.3 σ)
- lake env             maxrss                   2.4%  (224.9 σ)
- stdlib               instantiate metavars    17.9%   (14.1 σ)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5362 has successfully built against this PR. (2024-09-16 10:35:04) View Log

[kim-em]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6470afe.
There were significant changes against commit 5eea835:

  Benchmark            Metric         Change
  ====================================================
+ binarytrees.st       task-clock      -3.6% (-20.8 σ)
+ binarytrees.st       wall-clock      -3.6% (-20.7 σ)
- lake build no-op     maxrss           1.6% (251.2 σ)
- lake config elab     maxrss           2.2% (403.5 σ)
- lake config import   instructions     1.2%  (13.8 σ)
- lake config import   maxrss           2.4% (424.6 σ)
+ lake config import   task-clock      -9.1% (-12.2 σ)
+ lake config import   wall-clock      -9.1% (-12.1 σ)
- lake config tree     instructions     1.2%  (30.2 σ)
- lake config tree     maxrss           2.3% (119.1 σ)
- lake env             instructions     1.3%  (39.4 σ)
- lake env             maxrss           2.4% (288.1 σ)
+ unionfind            task-clock     -18.3% (-20.0 σ)
+ unionfind            wall-clock     -18.3% (-19.9 σ)

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6470afe.
There were significant changes against commit 5eea835:

  Benchmark            Metric         Change
  ====================================================
+ binarytrees.st       task-clock      -3.6% (-20.8 σ)
+ binarytrees.st       wall-clock      -3.6% (-20.7 σ)
- lake build no-op     maxrss           1.6% (251.2 σ)
- lake config elab     maxrss           2.2% (403.5 σ)
- lake config import   instructions     1.2%  (13.8 σ)
- lake config import   maxrss           2.4% (424.6 σ)
+ lake config import   task-clock      -9.1% (-12.2 σ)
+ lake config import   wall-clock      -9.1% (-12.1 σ)
- lake config tree     instructions     1.2%  (30.2 σ)
- lake config tree     maxrss           2.3% (119.1 σ)
- lake env             instructions     1.3%  (39.4 σ)
- lake env             maxrss           2.4% (288.1 σ)
+ unionfind            task-clock     -18.3% (-20.0 σ)
+ unionfind            wall-clock     -18.3% (-19.9 σ)

[hargoniX]

Talked with Mac, he thinks these perf diffs are acceptable.