diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index c9c7a2e09d..0f0aac19d2 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/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
diff --git a/tests/lean/run/try_panic.lean b/tests/lean/run/try_panic.lean
new file mode 100644
index 0000000000..38a694735a
--- /dev/null
+++ b/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?