Cannot use binderNameHint to control binders of simp congruence rules

[nomeata]

In #6947 we added a gadget to give more control over binder names when rewriting. It was pointed out on Zulip that losing binder names while simp’ing is seriously annoying, but unfortunately the given example isn't covered by binderNameHint so far, because the binder is lost due to a congr rule, not due to rewriting. Here is a mathlib free example:

section no_congr
/--
error: tactic 'fail' failed
xs : List Nat
⊢ xs = List.map (fun y => 1 + y) xs
-/
#guard_msgs in
example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
  simp
  fail

end no_congr

section with_congr

/--
info: List.map_congr_left.{u_1, u_2} {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹}
  (h : ∀ (a : α✝), a ∈ l → f a = g a) : List.map f l = List.map g l
-/
#guard_msgs in
#check List.map_congr_left

attribute [local congr] List.map_congr_left

/--
error: tactic 'fail' failed
xs : List Nat
⊢ xs = List.map (fun a => 1 + a) xs
-/
#guard_msgs in
example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
  simp -- NB: Changes variable name!
  fail

end with_congr

section with_congr_hint

-- Trying to use the binderNameHint on a congruence rule


--  this loops: 
theorem List.map_congr_left' {f g : α → β}  (h : ∀ (a : α), a ∈ l → (f a = g a)) : List.map f l = List.map (fun x => binderNameHint x f (g x)) l  :=
  List.map_congr_left h

-- this is not effective
theorem List.map_congr_left'' {f g : α → β}  (h : ∀ (a : α), a ∈ l → (binderNameHint a f (f a) = g a)) : List.map f l = List.map g l  := List.map_congr_left h

attribute [congr] List.map_congr_left''

/--
error: tactic 'fail' failed
xs : List Nat
⊢ xs = List.map (fun a => 1 + a) xs
-/
#guard_msgs in
example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
  simp -- the binderNameHint is not effective on congruence rules yet :-()
  fail

end with_congr_hint

It might help to insert something like

let rhs ← if type.hasBinderNameHint then rhs.resolveBinderNameHint else pure rhs

on the premises produced from applying a congr rule. Then the last variant tried above should work.

Context

https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Possible.20improvements.20to.20Lean.2FMathlibiption of what actually happens]

Versions

Lean 4.18.0-nightly-2025-02-11

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.