experiment: fix various eta issues

[arthur-adjedj]

This PR is an experiment in fixing various issues defeq issues related to eta-expansions, and should not be merged. The fixes are minimal in that they do not try to alter much of the codebase, and should incur some performance penalty. Some of them could be alleviated through various refactors. One goal of this draft is to measure the perf impact of the most naive approach to those fixes.

Closes #2258, #3213, #12520 and, more unexpectedly, #2237.

The fixes are as follows:

For #2258 : Expand the unit-like criteria to handle Pi types whose codomain is unit-like, and structures whose fields are all unit-like or proof-irrelevant.

For #3213: Expand the condition for which the major of a recursor can be eta-expanded. Namely, subsingleton structures such as And should be eta-expanded in this situation.

For #12520:

• In isDefEqEta, eta-expand partial recursor applications when the major is missing and is an eta-expandable structure.
• In isDefEqEtaStruct, eta-expand partial constructor applications.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-21 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-02-21 23:12:38)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12636 build failed against this PR. (2026-02-21 23:17:00) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12636 build failed against this PR. (2026-02-22 00:50:12) View Log

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12636 build failed against this PR. (2026-02-22 21:12:46) View Log

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 063264c against 527a07b are in! @arthur-adjedj

• 🟥 build exited with code 2
• 🟥 other exited with code 2

No significant changes detected.

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 3411e8c against 527a07b are in! @arthur-adjedj

• 🟥 build//instructions: +38.5G (+0.31%)

Large changes (2🟥)

• 🟥 big_struct_dep1//instructions: +813.7M (+12.80%)
• 🟥 simp_local//instructions: +3.9G (+8.58%)

Medium changes (10🟥)

• 🟥 Init.Data.BitVec.Lemmas//instructions: +665.8M (+0.53%)
• 🟥 Std.Data.DHashMap.Internal.RawLemmas//instructions: +2.3G (+0.88%)
• 🟥 Std.Data.Internal.List.Associative//instructions: +412.0M (+0.52%)
• 🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.1G (+0.69%)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.0G (+0.47%)
• 🟥 build/module/Std.Do.Triple.SpecLemmas//instructions: +1.0G (+3.07%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: +1.0G (+5.55%) (reduced significance based on absolute threshold)
• 🟥 bv_decide_rewriter.lean//instructions: +96.8M (+0.89%)
• 🟥 grind_bitvec2.lean//instructions: +1.4G (+0.67%)
• 🟥 grind_list2.lean//instructions: +330.6M (+0.57%)

Small changes (151🟥)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-12636 build failed against this PR. (2026-02-23 19:19:21) View Log

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 2b6be12 against 527a07b are in! @arthur-adjedj

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +38.3G (+0.31%)

Large changes (2🟥)

• 🟥 elab/big_struct_dep1//instructions: +814.2M (+12.80%)
• 🟥 elab/simp_local//instructions: +3.9G (+8.57%)

Medium changes (9🟥)

• 🟥 build/module/Std.Data.DHashMap.RawLemmas//instructions: +1.1G (+0.69%)
• 🟥 build/module/Std.Do.Triple.SpecLemmas//instructions: +1.0G (+3.12%) (reduced significance based on absolute threshold)
• 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv//instructions: +1.0G (+5.53%) (reduced significance based on absolute threshold)
• 🟥 elab/bv_decide_rewriter//instructions: +97.2M (+0.90%)
• 🟥 elab/grind_bitvec2//instructions: +1.3G (+0.67%)
• 🟥 elab/grind_list2//instructions: +328.6M (+0.57%)
• 🟥 misc/import Init.Data.BitVec.Lemmas//instructions: +664.5M (+0.53%)
• 🟥 misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: +2.3G (+0.89%)
• 🟥 misc/import Std.Data.Internal.List.Associative//instructions: +419.1M (+0.53%)

Small changes (156🟥)

Too many entries to display here. View the full report on radar instead.

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 5422814 against 527a07b are in! @arthur-adjedj

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +26.1G (+0.21%)

Large changes (2🟥)

• 🟥 elab/big_struct_dep1//instructions: +778.1M (+12.24%)
• 🟥 elab/simp_local//instructions: +3.4G (+7.48%)

Medium changes (5🟥)

• 🟥 elab/bv_decide_rewriter//instructions: +84.2M (+0.78%)
• 🟥 elab/grind_bitvec2//instructions: +976.9M (+0.48%)
• 🟥 elab/grind_list2//instructions: +216.3M (+0.37%)
• 🟥 misc/import Init.Data.BitVec.Lemmas//instructions: +436.0M (+0.35%)
• 🟥 misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: +2.0G (+0.77%)

Small changes (88🟥)

Too many entries to display here. View the full report on radar instead.

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 467c610 against 527a07b are in! @arthur-adjedj

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +18.5G (+0.15%)

Large changes (1🟥)

• 🟥 elab/simp_local//instructions: +777.8M (+1.72%)

Medium changes (1✅, 1🟥)

• ✅ elab/big_struct_dep1//instructions: -96.3M (-1.52%)
• 🟥 elab/grind_bitvec2//instructions: +660.5M (+0.33%)

Small changes (48🟥)

Too many entries to display here. View the full report on radar instead.

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for b586ad1 against 527a07b are in! @arthur-adjedj

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +19.9G (+0.16%)

Large changes (1🟥)

• 🟥 elab/simp_local//instructions: +779.9M (+1.72%)

Medium changes (1✅, 1🟥)

• ✅ elab/big_struct_dep1//instructions: -96.8M (-1.52%)
• 🟥 elab/grind_bitvec2//instructions: +692.4M (+0.34%)

Small changes (49🟥)

Too many entries to display here. View the full report on radar instead.

[arthur-adjedj]

!bench

[leanprover-radar]

Benchmark results for 4c08fdd against 527a07b are in! @arthur-adjedj

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +22.3G (+0.18%)

Large changes (1🟥)

• 🟥 elab/simp_local//instructions: +3.3G (+7.39%)

Medium changes (2🟥)

• 🟥 elab/grind_bitvec2//instructions: +772.6M (+0.38%)
• 🟥 elab/grind_list2//instructions: +224.6M (+0.39%)

Small changes (78🟥)

Too many entries to display here. View the full report on radar instead.