From 9c245d5531ad28fb491b3febdf7223134fdce1af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 18 Apr 2026 00:47:53 +0200
Subject: [PATCH] test: add regression test for `Sym.simp` eta-reduction
 (#13416) (#13452)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds a direct regression test for issue #13416. It exercises
`Std.HashMap.getElem_insert`, whose `dom` argument is a lambda closing
over pattern variables, and checks that the discrimination tree lookup
finds the theorem once the target's `dom` lambda is eta-reduced.

The underlying fix landed in #13448; this test pins the specific MWE
from the original issue so a regression would surface immediately.

Closes #13416

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
---
 tests/elab/sym_issue_13416.lean | 39 +++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 tests/elab/sym_issue_13416.lean

diff --git a/tests/elab/sym_issue_13416.lean b/tests/elab/sym_issue_13416.lean
new file mode 100644
index 0000000000..ee4e2f64af
--- /dev/null
+++ b/tests/elab/sym_issue_13416.lean
@@ -0,0 +1,39 @@
+import Lean.Meta.Sym
+import Std.Data.HashMap.Lemmas
+
+open Lean Meta Sym Simp in
+/--
+info: lhs: (Std.HashMap.emptyWithCapacity.insert "foo" 42)["foo"]
+---
+info: disc tree lookup match count: 1
+-/
+#guard_msgs in
+#eval show MetaM Unit from do
+  -- Insert `HashMap.getElem_insert` into a fresh Theorems tree.
+  -- Its `dom` argument is `fun m a => Membership.mem m a` with loose bvars → key `.other`
+  let thm ← mkTheoremFromDecl ``Std.HashMap.getElem_insert
+  let tree : Theorems := ({} : Theorems).insert thm
+
+  -- Build a concrete expression that should match.
+  -- Its `dom` argument is the same lambda but closed → etaReduce → key `.const Membership.mem 3`
+  let lhs ← do
+    let ty ← Lean.Elab.Term.TermElabM.run' (ctx := {}) do
+      return ← Lean.Elab.Term.elabTerm
+        (← `(((Std.HashMap.emptyWithCapacity : Std.HashMap String Nat).insert "foo" 42)["foo"]'(by simp) = 42))
+        none
+    let ty ← instantiateMVars ty
+    let some (_, lhs, _) := ty.eq? | throwError "not eq"
+    pure lhs
+
+  logInfo m!"lhs: {lhs}"
+
+  guard <| lhs.getAppFn.constName? == some ``GetElem.getElem
+  guard <| lhs.getAppNumArgs == 8
+
+  -- Confirm the dom argument is eta-reducible in the concrete expression
+  let dom := lhs.getAppArgs[3]!
+  guard dom.isLambda
+  guard <| !(Lean.Expr.eta dom).isLambda
+
+  let nMatches := (tree.getMatchWithExtra lhs).size
+  logInfo m!"disc tree lookup match count: {nMatches}"