`simp` does not match in expressions involving dependent function types

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Apparently simp is not able to show that if a = b then f a = f b if f is an ordinary (non-dependent) function type, but is built up from dependent-function types (so it's not "obviously" non-dependent).

Context

Spotted during PR review of code using Mathlib's Function.update (which supports dependent functions, but was being used for an ordinary function).

• Original Mathlib PR: #32959
• Zulip discussion thread: #mathlib4 > Simp fails to apply with `Function.update`

Steps to Reproduce

Code example:

universe u v

variable {α : Type u} [DecidableEq α]

/-- Mathlib's `Function.update` allowing dependent functions
(copied from Mathlib.Logic.Function.Basic) -/
def dupdate {β : α → Type v}
    (f : ∀ a, β a) (a' : α) (v : β a') (a : α) : β a :=
  if h : a = a' then Eq.ndrec v h.symm else f a

theorem foo (f : Nat → Nat) (a b : Nat) (hab : a = b) :
    (dupdate f 0 1) a = (dupdate f 0 1) b := by
  simp only [hab] -- fails, but `rw [hab]` works

/-- Non-dependent version of `Function.update` -/
def ndupdate {β : Type v}
    (f : α → β) (a' : α) (v : β) (a : α) : β :=
  if a = a' then v else f a

theorem foo2 (f : Nat → Nat) (a b : Nat) (hab : a = b) :
    (ndupdate f 0 1) a = (ndupdate f 0 1) b := by
  simp only [hab] -- works

Expected behavior: The simp only in the proof of foo should close the goal.

Actual behavior: It doesn't match on the argument of dupdate f 0 1 (but rw [hab] does match, and simp only [hab] works in foo2 with the non-dependent version).

Versions

Tested with Lean 4.28.0-rc1 and 4.29.0-nightly-2026-02-14 (identical behaviour in both).

Additional Information

Quoting comment from Joachim Breitner (@nomeata) on Zulip:

It's not a bug, at most a missing feature.

The component in question is probably the simp congruence theorem generation. I wonder if for functions where the dependency depends on some higher order argument, like here or in match statements, one could create specialized congr theorems for when that higher order function is actually constant.

But it's not a simple change, so don't hold your breath.

An issue to record the desires for this and to collect instances would be appreciated.

Impact

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

Start with the self-contained Lean reproducer in the issue and compare the failing simp only [hab] proof with the working rw [hab] proof. Investigate simp congruence theorem generation, as suggested in the issue. Done means the dependent dupdate example closes with simp only [hab] while the non-dependent example continues to work.