fix: getEqnsFor? should not panic on matchers

When a theorem's type contains a match expression, calling `getEqnsFor?`
on the generated matcher would panic with "duplicate normalized declaration name".

This occurred because matchers have their equations generated separately by
`Lean.Meta.Match.MatchEqs`, but `shouldGenerateEqnThms` didn't check for this,
leading to conflicting equation theorem names.

The fix makes `shouldGenerateEqnThms` return `false` for matchers, since their
equations are already handled by the dedicated matcher equation infrastructure.

Closes #11461

🤖 Prepared with Claude Code

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

Co-Authored-By: Claude <[email protected]>

Author: kim-em

src/Lean/Meta/Eqns.lean

@@ -150,9 +150,13 @@ def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
     throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
   getEqnsFnsRef.modify (f :: ·)
 
-/-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
+/-- Returns `true` iff `declName` is a definition and its type is not a proposition.
+    Returns `false` for matchers since their equations are handled by `Lean.Meta.Match.MatchEqs`. -/
 private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
   if let some { kind := .defn, sig, .. } := (← getEnv).findAsync? declName then
+    -- Matcher equations are handled separately in Lean.Meta.Match.MatchEqs
+    if isMatcherCore (← getEnv) declName then
+      return false
     return !(← isProp sig.get.type)
   else
     return false

tests/lean/run/try_panic.lean

@@ -0,0 +1,35 @@
+import Lean
+
+/-!
+# Regression test: getEqnsFor? should not panic on matchers
+
+Previously, when a theorem had a match expression in its type (e.g. `bar.match_1`),
+calling `getEqnsFor?` on the matcher would panic with "duplicate normalized declaration name".
+
+This was fixed by making `shouldGenerateEqnThms` return `false` for matchers, since
+matcher equations are handled separately by `Lean.Meta.Match.MatchEqs`.
+-/
+
+-- A theorem with a match expression in its type creates a matcher `bar.match_1`
+theorem bar : (match (0 : Nat) with | 0 => 0 | _ => 1) = 0 := by native_decide
+
+-- getEqnsFor? on a matcher should return none (not panic)
+/-- info: eqns: none -/
+#guard_msgs in
+#eval do
+  let eqns ← Lean.Meta.getEqnsFor? `bar.match_1
+  IO.println s!"eqns: {eqns}"
+
+-- try? should not panic when encountering matchers in the goal
+-- (it may fail to find suggestions, but should not panic)
+/--
+info: Try these:
+  [apply] rfl
+  [apply] simp
+  [apply] simp only
+  [apply] grind
+  [apply] grind only
+  [apply] simp_all
+-/
+#guard_msgs in
+theorem bar' : (match (0 : Nat) with | 0 => 0 | _ => 1) = 0 := by try?