diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 43bf97a60cb1..fa9ad77d6e9e 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -17,7 +17,7 @@ register_builtin_option backward.isDefEq.lazyProjDelta : Bool := {
 }
 
 register_builtin_option backward.isDefEq.lazyWhnfCore : Bool := {
-  defValue := true
+  defValue := false
   descr    := "specifies transparency mode when normalizing constraints of the form `(f a).i =?= s`, if `true` only reducible definitions and instances are unfolded when reducing `f a`. Otherwise, the default setting is used"
 }
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
index b5a96db49450..3c96d5aa26e3 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -205,21 +205,27 @@ where
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateLeft)
           dsimp only at heaig
           assumption
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (by
+          simp only [res]
+          exact AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateLeft) ..)⟩
       | .rotateRight distance =>
         let res := bitblast.blastRotateRight eaig ⟨evec, distance⟩
         have := by
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastRotateRight)
           dsimp only at heaig
           assumption
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (by
+          simp only [res]
+          exact AIG.LawfulVecOperator.le_size (f := bitblast.blastRotateRight) ..)⟩
       | .arithShiftRightConst distance =>
         let res := bitblast.blastArithShiftRightConst eaig ⟨evec, distance⟩
         have := by
           apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastArithShiftRightConst)
           dsimp only at heaig
           assumption
-        ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩
+        ⟨⟨res, this⟩, cache.cast (by
+          simp only [res]
+          exact AIG.LawfulVecOperator.le_size (f := bitblast.blastArithShiftRightConst) ..)⟩
       | .reverse =>
         let res := bitblast.blastReverse eaig evec
         have := by
@@ -250,7 +256,9 @@ where
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAppend)
         dsimp only at hlaig hraig
         omega
-      ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩
+      ⟨⟨res, this⟩, cache.cast (by
+        simp only [res]
+        exact AIG.LawfulVecOperator.le_size (f := bitblast.blastAppend) ..)⟩
     | .replicate n expr h =>
       let ⟨⟨⟨aig, expr⟩, haig⟩, cache⟩ := goCache aig expr cache
       let res := bitblast.blastReplicate aig ⟨n, expr, h⟩
@@ -258,7 +266,9 @@ where
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate)
         dsimp only at haig
         assumption
-      ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩
+      ⟨⟨res, this⟩, cache.cast (by
+        simp only [res]
+        exact AIG.LawfulVecOperator.le_size (f := bitblast.blastReplicate) ..)⟩
     | .extract start len expr =>
       let ⟨⟨⟨eaig, evec⟩, heaig⟩, cache⟩ := goCache aig expr cache
       let res := bitblast.blastExtract eaig ⟨evec, start⟩
@@ -266,7 +276,9 @@ where
         apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastExtract)
         dsimp only at heaig
         exact heaig
-      ⟨⟨res, this⟩, cache.cast (AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩
+      ⟨⟨res, this⟩, cache.cast (by
+        simp only [res]
+        exact AIG.LawfulVecOperator.le_size (f := bitblast.blastExtract) ..)⟩
     | .shiftLeft lhs rhs =>
       let ⟨⟨⟨aig, lhs⟩, hlaig⟩, cache⟩ := goCache aig lhs cache
       let ⟨⟨⟨aig, rhs⟩, hraig⟩, cache⟩ := goCache aig rhs cache
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
index fb5e48ff543d..29d0f4ea6b11 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
@@ -227,6 +227,11 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size
       exact h1
     have h4 : idx < (mkFullAdder aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by
+      /-
+      Without the unfolding of `mkFullAdder`, `apply` will pick the wrong `f`, and simply adding
+      `(f := mkFullAdderCarry)` runs into the heartbeat limit.
+      -/
+      simp only [mkFullAdder]
       apply AIG.LawfulOperator.lt_size_of_lt_aig_size
       exact h3
     rw [go_decl_eq (w := w) (curr := curr + 1) (h1 := h4)]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
index 94d51d73ad1e..769fd2e26423 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Pred.lean
@@ -51,7 +51,9 @@ def bitblast (aig : AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return ai
         apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkUlt)
         dsimp only at hlhs hrhs
         omega
-      ⟨⟨res, this⟩, cache⟩
+      ⟨⟨res, this⟩, by
+        simp only
+        exact cache⟩
   | .getLsbD expr idx =>
     /-
     Note: This blasts the entire expression up to `w` despite only needing it up to `idx`.