feat: auto eta-expand structures in grind when equality with constructor is present

[kim-em]

This PR adds Eq-triggered eta-expansion for structures in grind. When grind internalizes Eq α a b where one side is a structure constructor and the other isn't, it eta-expands the non-constructor side. This lets grind go from field equalities to structure equality without requiring @[grind] or @[grind ext] on the structure type.

For example, this now works without any annotation on LoopRange:

structure LoopRange where
  start : Nat
  end_ : Option Nat

def isZero (r : LoopRange) : Prop := r = ⟨0, some 0⟩
def isZeroVar (r : LoopRange) : Prop :=
  match r.end_ with
  | some x => r.start = 0 ∧ x = 0
  | none => False

example (r : LoopRange) : isZeroVar r ↔ isZero r := by
  unfold isZeroVar isZero; grind

Previously grind would deduce r.start = 0 and r.end_ = some 0 but couldn't reconstruct r = ⟨0, some 0⟩ unless LoopRange was registered with @[grind ext].

The approach is more targeted than unconditionally eta-expanding all structure terms — it only fires when a constructor appears in an equality, which avoids performance issues from cascading expansions on types like nested Prod.

Side effect: grind now proves additional theorems in the #grind_lint test suite (e.g. Array.get_max?, Array.min_mem), so expected outputs are updated.

🤖 Prepared with Claude Code

[kim-em]

!radar

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto e8048291010c815d0d30926924e7ad7afc18b1c0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-10 03:55:41)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 71ff36621103dfab119dfbead39dea3995d5832d --onto a165292462a973c20d3cc8c8b23a3ac2334a2a4a. You can force reference manual CI using the force-manual-ci label. (2026-03-10 03:55:44)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-09 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-03-10 11:30:15)

[kim-em]

!radar

[leanprover-radar]

Benchmark results for 474e02b against 71ff366 are in. There are no significant changes. @kim-em

• 🟥 build//instructions: +1.7G (+0.01%)

Medium changes (1🟥)

• 🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult//instructions: +1.2G (+2.32%) (reduced significance based on absolute threshold)

Small changes (3✅, 3🟥)

• 🟥 build/module/Lean.Meta.Tactic.Grind.Internalize//instructions: +703.6M (+2.87%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas//instructions: +77.8M (+0.41%)
• 🟥 build/module/Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult//instructions: +52.7M (+0.41%)
• ✅ compiled/unionfind//task-clock: -91ms (-9.34%)
• ✅ compiled/unionfind//wall-clock: -91ms (-9.29%)
• ✅ elab/bv_decide_realworld//wall-clock: -40ms (-3.36%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12860 has successfully built against this PR. (2026-03-10 12:26:49) View Log