[#14805] feat: special case single-child nodes in DiscrTree

[downstream-lean4]

This is the adaptation PR for leanprover/lean4#14805.

[downstream-lean4]

Build report for downstream: follow upstream PR

Stayed green

Repo	Critical	Build	Test	Lint
aesop	✅	✅ in 18s	✅ in 5s	⏭️
batteries	✅	✅ in 14s	✅ in 4s	✅ in 2s
import-graph	✅	✅ in 3s	✅ in 3s	⏭️
lean4-cli	✅	✅ in 3s	✅ in 0s	⏭️
mathlib4	✅	✅ in 1167s	✅ in 48s	✅ in 93s
plausible	✅	✅ in 3s	✅ in 2s	⏭️
ProofWidgets4	✅	✅ in 6s	✅ in 1s	⏭️
quote4	✅	✅ in 6s	✅ in 1s	⏭️
reference-manual	✅	✅ in 79s	⏭️	⏭️
BibtexQuery		✅ in 3s	⏭️	⏭️
comparator		✅ in 3s	⏭️	⏭️
cslib		✅ in 37s	✅ in 8s	✅ in 3s
doc-gen4		✅ in 15s	⏭️	⏭️
illuminate		✅ in 8s	✅ in 10s	⏭️
lean4-unicode-basic		✅ in 4s	⏭️	⏭️
lean4export		✅ in 3s	✅ in 7s	⏭️
LeanSearchClient		✅ in 2s	✅ in 0s	⏭️
leansqlite		✅ in 9s	✅ in 16s	⏭️
repl		✅ in 4s	✅ in 61s	⏭️
verso		✅ in 128s	✅ in 83s	⏭️
verso-slides		✅ in 18s	✅ in 6s	⏭️
verso-web-components		✅ in 35s	⏭️	⏭️

View run

[leanprover-radar]

Benchmark results for 33f1924 against 92e8256 are in. There are significant results. @robsimmons

• ✅ build//instructions: -1.1T (-0.75%)

Large changes (2✅)

• ✅ open-mathlib//maxrss: -104MiB (-3.62%)
• and 1 hidden

Small changes (494✅)

• ✅ build/module/Aesop.BaseM//instructions: -24.2M (-1.51%)
• ✅ build/module/Aesop.Builder.Apply//instructions: -23.2M (-1.36%)
• ✅ build/module/Aesop.Builder.Cases//instructions: -24.5M (-1.38%)
• ✅ build/module/Aesop.Builder.Constructors//instructions: -24.9M (-1.54%)
• ✅ build/module/Aesop.Builder.Default//instructions: -22.5M (-1.40%)
• ✅ build/module/Aesop.Builder.NormSimp//instructions: -24.5M (-1.36%)
• ✅ build/module/Aesop.Builder.Unfold//instructions: -23.7M (-1.40%)
• ✅ build/module/Aesop.BuiltinRules.Ext//instructions: -23.9M (-1.23%)
• ✅ build/module/Aesop.BuiltinRules.Intros//instructions: -23.3M (-1.28%)
• ✅ build/module/Aesop.BuiltinRules.Rfl//instructions: -25.4M (-1.65%)
• ✅ build/module/Aesop.BuiltinRules.Split//instructions: -24.3M (-1.19%)
• ✅ build/module/Aesop.Check//instructions: -24.1M (-1.41%)
• ✅ build/module/Aesop.ElabM//instructions: -24.4M (-1.69%)
• ✅ build/module/Aesop.Forward.LevelIndex//instructions: -21.1M (-1.86%)
• ✅ build/module/Aesop.Forward.PremiseIndex//instructions: -20.3M (-1.79%)
• ✅ build/module/Aesop.Forward.State.ApplyGoalDiff//instructions: -23.6M (-1.17%)
• ✅ build/module/Aesop.Forward.State.Initial//instructions: -22.9M (-1.17%)
• ✅ build/module/Aesop.Forward.State.UpdateGoal//instructions: -24.0M (-1.39%)
• ✅ build/module/Aesop.Frontend.Extension.Init//instructions: -24.0M (-1.70%)
• ✅ build/module/Aesop.Frontend.Extension//instructions: -24.2M (-0.87%)
• and 474 more