fix: better structural recursion equations

[Rob23oba]

This PR replaces the previous tactic-based structural equation prover with a more direct and reliable approach. For example, these two examples now work:

def test1 (b : Bool) (l : List Bool) : Bool :=
  b && l.casesOn true fun x t => test1 x t

def test2 (l : List Bool) (n : Nat) : Nat :=
  if n = n + n then
    match l with
    | [] => n
    | _ :: xs => test2 xs n
  else
    3

#print test1.eq_def -- previously got stuck
#print test2.eq_def -- previously got maximum recursion depth reached

TODO: I still have to figure out the edge case | .let a b => denote (b (denote a)).

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for 3d030c6 against dec70ee are in. There are significant results. @Rob23oba

• 🟥 build exited with code 1
• 🟥 other exited with code 1

No significant changes detected.

[Rob23oba]

!bench

[leanprover-radar]

Benchmark results for 9a71d19 against dec70ee are in. There are significant results. @Rob23oba

• ✅ build//instructions: -29.7G (-0.26%)

New metrics (16✅, 14🟥)

• 🟥 elab/let_to_have_chain//cycles: +21.2M (+0.98%)
• 🟥 elab/let_to_have_chain//instructions: +3.4M (+0.11%)
• ✅ elab/let_to_have_chain//maxrss: -4MiB (-0.25%)
• 🟥 elab/let_to_have_chain//task-clock: +3ms (+0.83%)
• 🟥 elab/let_to_have_chain//wall-clock: +3ms (+0.76%)
• 🟥 elab/let_to_have_closed_body//cycles: +3.0M (+0.13%)
• 🟥 elab/let_to_have_closed_body//instructions: +1.7M (+0.05%)
• ✅ elab/let_to_have_closed_body//maxrss: -4MiB (-0.24%)
• ✅ elab/let_to_have_closed_body//task-clock: -3ms (-0.62%)
• ✅ elab/let_to_have_closed_body//wall-clock: -2ms (-0.53%)
• ✅ elab/let_to_have_nested//cycles: -526.2M (-2.28%)
• 🟥 elab/let_to_have_nested//instructions: +512.0k (+0.00%)
• ✅ elab/let_to_have_nested//maxrss: -2MiB (-0.12%)
• ✅ elab/let_to_have_nested//task-clock: -89ms (-2.14%)
• ✅ elab/let_to_have_nested//wall-clock: -91ms (-2.16%)
• 🟥 elab/sym_let_to_have_chain//cycles: +12.9M (+0.54%)
• 🟥 elab/sym_let_to_have_chain//instructions: +5.4M (+0.16%)
• ✅ elab/sym_let_to_have_chain//maxrss: -7MiB (-0.36%)
• 🟥 elab/sym_let_to_have_chain//task-clock: +3ms (+0.78%)
• 🟥 elab/sym_let_to_have_chain//wall-clock: +4ms (+0.89%)
• and 10 more

Large changes (4✅)

• ✅ build/module/Std.Data.DTreeMap.Internal.Model//instructions: -11.2G (-19.06%)
• ✅ build/stat/imported bytes//bytes: -2GiB (-1.89%)
• ✅ size/Init/.olean//bytes: -2MiB (-2.15%)
• ✅ size/all/.olean//bytes: -6MiB (-1.70%)

Medium changes (9✅)

• ✅ build/module/Init.Data.Int.Linear//instructions: -1.1G (-4.50%)
• ✅ build/module/Init.Data.List.Impl//instructions: -1.4G (-19.55%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Grind.Ring.CommSolver//instructions: -3.3G (-9.63%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DHashMap.Internal.AssocList.Lemmas//instructions: -2.2G (-32.78%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Data.DTreeMap.Internal.WF.Lemmas//instructions: -2.2G (-5.57%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Basic//instructions: -1.5G (-15.29%) (reduced significance based on absolute threshold)
• ✅ build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure//instructions: -1.2G (-13.64%) (reduced significance based on absolute threshold)
• ✅ elab/cbv_leroy//instructions: -404.2M (-0.88%)
• ✅ misc/re-elab Init.Data.List.Basic//instructions: -9.9G (-7.13%)

Small changes (86✅, 5🟥)

• ✅ build/module/Init.Data.AC//instructions: -307.6M (-8.09%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Basic//instructions: -32.9M (-0.31%)
• ✅ build/module/Init.Data.Array.BasicAux//instructions: -54.0M (-3.81%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Bootstrap//instructions: -297.5M (-12.71%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.DecidableEq//instructions: -62.5M (-2.73%)
• ✅ build/module/Init.Data.Array.GetLit//instructions: -106.2M (-10.69%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Lemmas//instructions: -350.5M (-0.66%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.MapIdx//instructions: -314.3M (-3.61%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.OfFn//instructions: -86.9M (-4.48%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.Array.Range//instructions: -82.3M (-2.08%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.BitVec.Bitblast//instructions: -409.0M (-0.82%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.ByteArray.Bootstrap//instructions: -25.1M (-3.55%)
• ✅ build/module/Init.Data.Dyadic.Basic//instructions: -63.1M (-0.46%)
• ✅ build/module/Init.Data.Fin.Fold//instructions: -50.8M (-1.30%)
• ✅ build/module/Init.Data.Fin.Lemmas//instructions: -252.2M (-2.36%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.Attach//instructions: -87.4M (-1.10%)
• ✅ build/module/Init.Data.List.Basic//instructions: -979.1M (-7.52%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.BasicAux//instructions: -70.0M (-3.16%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.Control//instructions: -231.8M (-8.58%) (reduced significance based on absolute threshold)
• ✅ build/module/Init.Data.List.ControlImpl//instructions: -107.5M (-11.56%) (reduced significance based on absolute threshold)
• and 71 more

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-18 15:33:06)
• 🟡 Reference manual branch lean-pr-testing-14822 build against this PR didn't complete normally. (2026-08-21 16:02:08) View Log
• ✅ Reference manual branch lean-pr-testing-14822 has successfully built against this PR. (2026-08-21 16:02:11) View Log
• ✅ Reference manual branch lean-pr-testing-14822 has successfully built against this PR. (2026-08-21 20:26:15) View Log
• 🟡 Reference manual branch lean-pr-testing-14822 build against this PR didn't complete normally. (2026-08-21 20:28:15) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-14822 build failed against this PR. (2026-08-18 16:23:36) View Log
• 💥 Mathlib branch lean-pr-testing-14822 build failed against this PR. (2026-08-18 20:12:04) View Log
• ✅ Mathlib branch lean-pr-testing-14822 has successfully built against this PR. (2026-08-18 23:13:35) View Log
• ❌ Mathlib branch lean-pr-testing-14822 built against this PR, but testing failed. (2026-08-21 17:08:06) View Log
• ❌ Mathlib branch lean-pr-testing-14822 built against this PR, but testing failed. (2026-08-21 21:12:42) View Log