isDefEq can ignore the proofIrrelevance setting

Prerequisites

Please put an X between the brackets as you perform the following steps:

• 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

isDefEqArgsFirstPass in ExprDefEq implicitly encodes proof irrelevance, causing isDefEq to have some proof-irrelevance behavior regardless of the Lean.Meta.Context.proofIrrelevance setting.

When proof arguments are being compared, if neither is of the form fun x_1 ... x_n => ?m y_1 ... y_m, the argument is skipped unconditionally. This can be problematic if, for instance, the proof argument on one side has the form (p x) and the other has the form (p ?m). In this case, ?m will not be assigned to x due to proof irrelevance, regardless of the setting.

Context

I reported this issue on Zulip. Parts of the explanation above were provided by @kmill.

Steps to Reproduce

In the following code, observe the dbg_trace output.

import Lean
open Lean Meta Expr Elab Tactic Core

axiom p : Unit → ∃ x : Unit, True
noncomputable def concrete := fun x => (p x).choose

-- set_option trace.Meta.isDefEq true
#eval (do
  let value := (← getConstInfo ``concrete).value!
  let e1 := value.bindingBody!.instantiate1 (.const ``Unit.unit [])
  let e2 := value.bindingBody!.instantiate1 (← mkFreshExprMVar (Expr.const ``Unit []))
  withConfig (fun c => { c with proofIrrelevance := false }) do
    let _ ← isDefEq e1 e2
    dbg_trace (← instantiateMVars e2)
)

This code performs isDefEq on (p Unit.unit).choose and (p ?m).choose with the proofIrrelevance setting set to false.

Expected behavior: I expect ?m to be set to Unit.unit.

Although (p Unit.unit) and (p ?m) are proof arguments to the Exists.choose function, we have explicitly asked isDefEq to ignore proof irrelevance, so these arguments should not be skipped.

Actual behavior: The metavariable remains unassigned.

Versions

Lean 4.23.0-nightly-2025-07-28

Additional Information

N/A

Impact

I am developing a tactic and subsystem for Canonical that requires this functionality, by an update to isDefEq or by some workaround.

Start with isDefEqArgsFirstPass in ExprDefEq and the surrounding isDefEq implementation. Run the minimal Lean reproduction from the issue with proofIrrelevance := false, then trace the comparison of (p Unit.unit).choose and (p ?m).choose. Done means the behavior respects that setting and the metavariable is assigned as expected.