"found messy" can break proof irrelevance in `isDefEq`

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

isDefEqs "found messy" handling can cause proof arguments to be compared

Context

This causes several cases of the anti-pattern simp; rfl in byte array files.

Steps to Reproduce

class MyClass (f : outParam (Nat → Nat)) where

def test (f : outParam (Nat → Nat)) [MyClass f] (h : f 0 < 2) : Bool :=
  match f 0, h with
  | 0, _ => false
  | 1, _ => true

/--
error: Tactic `rfl` failed: equality lhs
  test f h₁
is not definitionally equal to rhs
  test f h₂

f : Nat → Nat
inst✝ : MyClass f
h₁ : f 0 < 2
h₂ : f 0 + 1 ≤ 2
⊢ test f h₁ = test f h₂
---
trace: [Meta.isDefEq] ❌️ test f h₁ =?= test f h₂
  [Meta.isDefEq] found messy f =?= f
  [Meta.isDefEq] found messy h₁ =?= h₂
  [Meta.isDefEq] ✅️ inst✝ =?= inst✝
  [Meta.isDefEq] ✅️ f =?= f
  [Meta.isDefEq] ❌️ h₁ =?= h₂
    [Meta.isDefEq] ❌️ f 0 < 2 =?= f 0 + 1 ≤ 2
      [Meta.isDefEq] ❌️ @LT.lt =?= @LE.le
      [Meta.isDefEq.onFailure] ❌️ f 0 < 2 =?= f 0 + 1 ≤ 2
      [Meta.isDefEq] ❌️ (f 0).lt 2 =?= (f 0 + 1).le 2
        [Meta.isDefEq] ❌️ Nat.lt =?= Nat.le
        [Meta.isDefEq.onFailure] ❌️ (f 0).lt 2 =?= (f 0 + 1).le 2
        [Meta.isDefEq.onFailure] ❌️ (f 0).lt 2 =?= (f 0 + 1).le 2
  [Meta.isDefEq.onFailure] ❌️ test f h₁ =?= test f h₂
  [Meta.isDefEq.onFailure] ❌️ test f h₁ =?= test f h₂
-/
#guard_msgs in
example (f : outParam (Nat → Nat)) [MyClass f] (h₁ : f 0 < 2) (h₂ : f 0 + 1 ≤ 2) : test f h₁ = test f h₂ := by
  set_option trace.Meta.isDefEq true in
  with_reducible eq_refl

Expected behavior: Just like usual, isDefEq ignores all proof arguments and succeeds.

Actual behavior: isDefEq found messy and compares the two proofs h₁ and h₂, which amounts to comparing the types. However, this fails under reducible transparency.

Versions

Lean 4.30.0-nightly-2026-03-28

Impact

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

Start with the minimal MyClass/test example and inspect the Meta.isDefEq trace, especially the found messy handling. Follow the isDefEq path that compares test f h₁ with test f h₂; done means proof arguments are ignored and the example succeeds under reducible transparency without comparing h₁ and h₂.