fix: bump transparency in isDefEqProj for class projections (#12633)

This PR makes `isDefEqProj` bump transparency to `.instances` (via
`withInstanceConfig`) when comparing the struct arguments of class
projections. This makes the behavior consistent with `isDefEqArgs`,
which already applies the same bump for instance-implicit parameters
when comparing function applications.

When a class field like `X.x` is marked `@[reducible]`, `isDefEqDelta`
unfolds it to `.proj` form. Previously, `isDefEqProj` compared the
struct arguments at the ambient transparency (`.reducible` in simp),
which meant instance definitions (which are `[implicit_reducible]`)
could not be unfolded, causing `eq_self` to fail. In the function
application form (`X.x inst` vs `X.x inst'`), `isDefEqArgs` correctly
bumps to `.instances` for the instance-implicit parameter. The `.proj`
path should behave the same way.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

src/Lean/Meta/ExprDefEq.lean

@@ -2020,13 +2020,23 @@ where
 
 private def isDefEqProj : Expr → Expr → MetaM Bool
   | .proj m i t, .proj n j s => do
+    /- When `m` is a class, the projection's parameter is instance-implicit.
+       We bump the transparency to `.instances` (via `withInstanceConfig`) so that
+       instance definitions (which are `[implicit_reducible]`) can be unfolded when comparing
+       the struct arguments. Without this bump, comparing `.proj` nodes produced by unfolding
+       a `[reducible]` class field fails because the struct arguments (`instX a` vs `instX b`)
+       are stuck at `.reducible`. This mirrors the transparency bump that `isDefEqArgs` applies
+       for instance-implicit parameters. -/
+    let fromClass := isClass (← getEnv) m
+    let isDefEqStructArgs (x : MetaM Bool) : MetaM Bool :=
+      if fromClass then withInstanceConfig x else x
     if (← read).inTypeClassResolution then
       -- See comment at `inTypeClassResolution`
-      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+      pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)
     else if !backward.isDefEq.lazyProjDelta.get (← getOptions) then
-      pure (i == j && m == n) <&&> Meta.isExprDefEqAux t s
+      pure (i == j && m == n) <&&> isDefEqStructArgs (Meta.isExprDefEqAux t s)
     else if i == j && m == n then
-      isDefEqProjDelta t s i
+      isDefEqStructArgs (isDefEqProjDelta t s i)
     else
       return false
   | .proj structName 0 s, v  => isDefEqSingleton structName s v

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -90,9 +90,22 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         -- `class` projection
         if (← getContext).isDeclToUnfold cinfo.name then
           /-
-          If user requested `class` projection to be unfolded, we set transparency mode to `.instances`,
-          and invoke `unfoldDefinition?`.
-          Recall that `unfoldDefinition?` has support for unfolding this kind of projection when transparency mode is `.instances`.
+          If user requested `class` projection to be unfolded (e.g., `simp [X.x]`), we set transparency
+          mode to `.instances` and invoke `unfoldDefinition?`.
+          Recall that `unfoldDefinition?` has support for unfolding this kind of projection when
+          transparency mode is `.instances`.
+
+          Note: this unfolds the projection function but may leave a `.proj` node that cannot be further
+          reduced. For example, given:
+          ```
+          def a' := 0; def b' := 0
+          class X where x : Nat
+          instance instX (n : Nat) : X where x := n
+          ```
+          `simp [X.x]` on `(instX a').x = (instX b').x` unfolds `X.x` to expose `.proj X 0 (instX a')`,
+          but cannot reduce further because `instX a'` is not a constructor application at `.reducible`.
+          The resulting goal `(instX a').1 = (instX b').1` is expected and reasonable: the user explicitly
+          requested the unfolding, and the projection is stuck because `a'` and `b'` are semireducible.
           -/
           let e? ← withReducibleAndInstances <| unfoldDefinition? e
           if e?.isSome then

tests/lean/run/test_simp_reducible_class.lean

@@ -0,0 +1,47 @@
+module
+
+/-!
+# Test: `simp` with `@[reducible]` class field projections
+
+When a class field like `X.x` is marked `@[reducible]`, `isDefEqDelta` unfolds it to `.proj` form.
+`isDefEqProj` must then bump transparency to `.instances` when comparing the struct arguments,
+since the projection's parameter is instance-implicit. Without this bump, `eq_self` fails because
+instances like `instX a` vs `instX b` are stuck at `.reducible`.
+-/
+
+namespace SimpReducibleClassField
+
+@[implicit_reducible] def a := 0
+@[implicit_reducible] def b := 0
+
+class X where
+  x : Nat
+
+instance instX (n : Nat) : X where
+  x := n
+
+-- Test 1: plain simp, semireducible X.x (works on master)
+-- isDefEqArgs bumps to .instances for instance-implicit param of X.x
+example : (instX a).x = (instX b).x := by simp
+
+-- Test 2: plain simp, @[reducible] X.x (BROKEN on master, fixed by isDefEqProj change)
+-- isDefEqDelta unfolds X.x to .proj form, isDefEqProj needs withInstanceConfig
+set_option allowUnsafeReducibility true in
+attribute [reducible] X.x in
+example : (instX a).x = (instX b).x := by simp
+
+-- Test 3: simp [X.x] with semireducible args exposes stuck .proj node
+-- reduceProjFn? unfolds X.x at .instances, but the .proj can't reduce further
+-- because instX a' is not a constructor app at .reducible. This is expected:
+-- the user explicitly requested the unfolding.
+def a' := 0
+def b' := 0
+
+/--
+error: unsolved goals
+⊢ (instX a').1 = (instX b').1
+-/
+#guard_msgs in
+example : (instX a').x = (instX b').x := by simp [X.x]
+
+end SimpReducibleClassField