`nomatch` causes "... was not added to the environment" error in `genMatchCongrEqns`

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

When you try to generate congruence equation lemmas for a nomatch through genMatchCongrEqns or something that uses it (e.g. grind), you get the following error:

Failed to realize constant xyz.match_n.congr_eq_1:
  Lean.Meta.realizeConst: _private.module.0.xyz.match_1.congr_eq_1 was not added to the environment

Steps to Reproduce

axiom Fin.succAbove {n : Nat} (i : Fin (n + 1)) (j : Fin n) : Fin (n + 1)

@[elab_as_elim]
axiom Fin.succAboveCases.{u} {n : Nat} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i)
  (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : α j

noncomputable def newPredAbove (p i : Fin (n + 1)) (hip : i ≠ p) : Fin n :=
  p.succAboveCases nofun (fun x _ => x) i hip

/--
error: Failed to realize constant newPredAbove.match_1.congr_eq_1:
  Lean.Meta.realizeConst: _private.«external:file:///lean-nightly/lean-nightly.lean».0.newPredAbove.match_1.congr_eq_1 was not added to the environment
---
error: Unknown constant `newPredAbove.match_1.congr_eq_1`
-/
#guard_msgs in
#print newPredAbove.match_1.congr_eq_1

Expected behavior: You just get an "Unknown identifier" error and an empty array returned in the corresponding genMatchCongrEqns call.

Actual behavior: genMatchCongrEqns fails with the error message mentioned above.

Versions

Lean 4.28.0-nightly-2025-12-15

Impact

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

Start by running the minimal reproducer and inspect the genMatchCongrEqns entry point, including the path used by grind. Compare the handling of a missing nomatch congruence equation with the expected unknown-identifier result; done means no realization failure and an empty result from genMatchCongrEqns.