feat: optimize computing `BinderInfo`s for discrimination trees

[kmill]

trafficstars

When computing paths for discrimination trees, currently it uses getFunInfoNArgs to calculate binder infos. This does many other calculations as well, and it also doesn't handle overapplied functions. Switches to a straightforward calculation that accumulates BinderInfos.

The effect of this is a reduction of 0.05% instructions when building mathlib. This is not worth reviewing for now.

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-3113 has successfully built against this PR. (2024-01-05 14:20:01) View Log
• ✅ Mathlib branch lean-pr-testing-3113 has successfully built against this PR. (2024-01-05 15:49:27) View Log
• 🟡 Mathlib branch lean-pr-testing-3113 build this PR didn't complete normally. (2024-04-17 20:30:17) View Log
• ✅ Mathlib branch lean-pr-testing-3113 has successfully built against this PR. (2024-04-17 22:18:03) View Log
• ✅ Mathlib branch lean-pr-testing-3113 has successfully built against this PR. (2024-05-09 22:42:31) View Log

[kmill]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1fa937db4e543546eb648901c4f08fe9cb558987. There were significant changes against commit d3e004932c1f5ac3946850692940512d381c7634:

  Benchmark   Metric                  Change
  ====================================================
+ stdlib      attribute application    -1.4% (-14.5 σ)