fix: binderNameHint with simp

[Rob23oba]

This PR fixes the behavior of rewriting foralls with simp and binderNameHint.

See discussion at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/binderNameHint.20.26.20simp/with/572625591

[nomeata]

Thanks! Unfortunately this touches code that's very deep in the stack, and fixes a problem with a (relatively) less critical component. So unless the changes deep down are clearly inconsequential to all the other components that may rely on the current ordering, this may be a problem for this PR.

[Rob23oba]

I don't see a reason why the binder names from isDefEq would matter other than something like binderNameHint (and even then, the change is mostly visual and you should only ever get a semantic difference when you use unhygienic tactics)

[Rob23oba]

For an explanation why this change makes sense: In a call of isDefEq a b, a is considered to be more variable and b more constant. You can see this convention with how ?a =?= ?b is handled: The left-hand side has priority for being assigned/changed and changes to the right-hand side are avoided unless ?a := ?b doesn't work out. In this context, a defeq check ∀ a, ?p a =?= ∀ b, q b should be more willing to change a to b than the other way around; thus the right-hand side binder name should be preferred.

[nomeata]

Right, I'm not worried about the change to isdefeq that only changes naming, but the one to kabstract

[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 23dc467ef5cbb34720e67e17f018f9e5d322ab7a --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-08 19:44:50)

[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 23dc467ef5cbb34720e67e17f018f9e5d322ab7a --onto 75d7f7eb227bc54dc6ea3d8ead090ee4180debaf. You can force reference manual CI using the force-manual-ci label. (2026-02-08 19:44:52)

[Rob23oba]

Oh, right; well I'd say that the previous behavior of kabstract was in fact wrong, consider this:

/--
error: unsolved goals
case h
⊢ ?h + 1 = 3

case h
⊢ Nat
---
error: No goals to be solved
-/
#guard_msgs in
example : True := by
  apply (fun (n : Nat) (h : Nat.succ n = 3) => trivial)
  · rewrite [Nat.succ_eq_add_one]
  · sorry

That's because it previously had the arguments to isDefEq in the wrong order; it should prefer changing the pattern by assigning metavariables in the pattern and not changing the value, so the pattern should be first (this is actually how simp does it already). A similar problem occurred in generalize:

/-- error: No goals to be solved -/
#guard_msgs in
example : True := by
  apply (fun (n : Nat) (h : 0 ≤ Nat.succ n) => trivial)
  · generalize Nat.succ _ = a
    simp
  · exact 0

I'm pretty sure that isDefEq is (mostly) symmetric modulo priority of assigning metavariables, so really, this change should only affect users of kabstract for the better (should I add these tests? If yes, where?).

[nomeata]

The main user of kabstract is rw, right? Making things more like they are with simp is probably a good sign. So is if nothing breaks in existing code.

It's useful to capture this corner case with a test (using rw, not meta programming, if you can). Such a test probably needs a good comment that the next person looking at it will know what's being tested for here.

Although I wouldn't be surprised if someone out there expects rw to instantiate MVars in the value of that's what it takes...