From af2444a140d51e3c97247814204fef6821d2ba76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Mon, 9 Feb 2026 18:45:58 +0000
Subject: [PATCH] perf: always zeta reduce let expressions in `cbv` (#12397)

This PR adds zeta reduction simproc to the pre step of `cbv`.
---
 src/Lean/Meta/Tactic/Cbv/Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean
index f1f43bdb91..f12ce75019 100644
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@@ -145,7 +145,7 @@ def cbvPre : Simproc :=
       isBuiltinValue <|> isProofTerm <|> skipBinders
   >>  isOpaqueApp
   >>  simpControlCbv
-    <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj)
+    <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj) <|> zetaReduce
 
 def cbvPost : Simproc :=
       evalGround