conv: "cannot select argument" with funlike coercions

[kmill]

Description

Function coercions are almost impossible to navigate in conv mode.

Context

In this Zulip thread, there's an example of an expression using a function coercion where it's impossible to access the argument to that coerced function using conv mode. Issue #2942 was meant to address this, but it wasn't the root issue, which is instead that the congr lemma generated in this case is too strict.

Steps to Reproduce

class DFunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  /-- The coercion from `F` to a function. -/
  coe : F → ∀ a : α, β a

structure MyFun (α β : Type) where
  toFun : α → β

instance : DFunLike (MyFun α β) α (fun _ => β) where
  coe f := f.toFun

example (a b : Nat) (h : a = b) (f : MyFun Nat Int) : DFunLike.coe f a = DFunLike.coe f b := by
  conv =>
    enter [1, 2] -- cannot select argument

Expected behavior: We select the a argument of the LHS.

Actual behavior: "cannot select argument"

Additional information

It's possible to navigate to the argument by breaking up the application in some way:

example (a b : Nat) (h : a = b) (f : MyFun Nat Int) : DFunLike.coe f a = DFunLike.coe f b := by
  conv =>
    enter [1]
    change (fun a => DFunLike.coe f a) a
    enter [1]
    rw [h]

Versions

Lean 4.12.0, commit c57d054
Target: arm64-apple-darwin24.0.0 macOS

Impact

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