From 03dc334f73259e1bae0b8f2b80a39a82e1de3df6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 6 Feb 2026 16:24:30 -0800
Subject: [PATCH] fix: simp `have` in `Sym` (#12370)

This PR fixes a proof construction bug in `Sym.simp`.

Closes #12336
---
 src/Lean/Meta/Sym/Simp/Have.lean  | 5 +++--
 tests/lean/run/sym_cbv_12336.lean | 5 +++++
 2 files changed, 8 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/sym_cbv_12336.lean

diff --git a/src/Lean/Meta/Sym/Simp/Have.lean b/src/Lean/Meta/Sym/Simp/Have.lean
index d0d648023c..95a3a61de9 100644
--- a/src/Lean/Meta/Sym/Simp/Have.lean
+++ b/src/Lean/Meta/Sym/Simp/Have.lean
@@ -318,12 +318,13 @@ For each application `f a`:
 -/
 def simpBetaApp (e : Expr) (fType : Expr) (fnUnivs argUnivs : Array Level)
     (simpBody : Simproc) : SimpM Result := do
-  return (← go e 0).1
+  let numArgs := argUnivs.size
+  return (← go e (numArgs - 1)).1
 where
   go (e : Expr) (i : Nat) : SimpM (Result × Expr) := do
     match e with
     | .app f a =>
-      let (rf, fType) ← go f (i+1)
+      let (rf, fType) ← go f (i-1)
       let r ← match rf, (← simp a) with
         | .rfl _, .rfl _ =>
           pure .rfl
diff --git a/tests/lean/run/sym_cbv_12336.lean b/tests/lean/run/sym_cbv_12336.lean
new file mode 100644
index 0000000000..3e1e8a82ab
--- /dev/null
+++ b/tests/lean/run/sym_cbv_12336.lean
@@ -0,0 +1,5 @@
+import Std
+set_option cbv.warning false
+
+def test : ((Std.TreeSet.empty : Std.TreeSet Nat).insertMany [1]).toList = [1] := by
+  conv => lhs; cbv