Apply suggestions from code review

Co-authored-by: Siddharth <siddu.druid@gmail.com>

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/EmbeddedConstraint.lean

@@ -51,7 +51,11 @@ def embeddedConstraintPass : Pass where
       let cfg ← PreProcessM.getConfig
       let targets ← goal.withContext getPropHyps
       let simpCtx ← Simp.mkContext
-        (config := { failIfUnchanged := false, maxSteps := cfg.maxSteps })
+        (config := {
+          failIfUnchanged := false,
+          implicitDefEqProofs := false, -- leanprover/lean4/pull/7509
+          maxSteps := cfg.maxSteps,
+        })
         (simpTheorems := relevantHyps)
         (congrTheorems := (← getSimpCongrTheorems))
       let ⟨result?, _⟩ ← simpGoal goal (ctx := simpCtx) (fvarIdsToSimp := targets)

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean

@@ -440,7 +440,11 @@ partial def enumsPass : Pass where
         (simprocs, relevantLemmas) ← addStructureSimpLemmas simprocs relevantLemmas
 
       let simpCtx ← Simp.mkContext
-        (config := { failIfUnchanged := false, maxSteps := cfg.maxSteps })
+        (config := {
+          failIfUnchanged := false,
+          implicitDefEqProofs := false, -- leanprover/lean4/pull/7509
+          maxSteps := cfg.maxSteps,
+        })
         (simpTheorems := relevantLemmas)
         (congrTheorems := ← getSimpCongrTheorems)
 

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/IntToBitVec.lean

@@ -59,7 +59,12 @@ def intToBitVecPass : Pass where
     let intToBvThms ← intToBitVecExt.getTheorems
     let cfg ← PreProcessM.getConfig
     let simpCtx ← Simp.mkContext
-      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps := cfg.maxSteps })
+      (config := {
+        failIfUnchanged := false,
+        zetaDelta := true,
+        implicitDefEqProofs := false, -- leanprover/lean4/pull/7509
+        maxSteps := cfg.maxSteps,
+      })
       (simpTheorems := #[intToBvThms])
       (congrTheorems := (← getSimpCongrTheorems))
 

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Rewrite.lean

@@ -31,7 +31,12 @@ def rewriteRulesPass : Pass where
     let cfg ← PreProcessM.getConfig
 
     let simpCtx ← Simp.mkContext
-      (config := { failIfUnchanged := false, zetaDelta := true, maxSteps := cfg.maxSteps })
+      (config := {
+        failIfUnchanged := false,
+        zetaDelta := true,
+        implicitDefEqProofs := false, -- leanprover/lean4/pull/7509
+        maxSteps := cfg.maxSteps,
+      })
       (simpTheorems := #[bvThms, sevalThms])
       (congrTheorems := (← getSimpCongrTheorems))
 

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean

@@ -82,7 +82,11 @@ where
       (simprocs, relevantLemmas) ← addStructureSimpLemmas simprocs relevantLemmas
       let cfg ← PreProcessM.getConfig
       let simpCtx ← Simp.mkContext
-        (config := { failIfUnchanged := false, maxSteps := cfg.maxSteps })
+        (config := {
+          failIfUnchanged := false,
+          implicitDefEqProofs := false, -- leanprover/lean4/pull/7509
+          maxSteps := cfg.maxSteps,
+        })
         (simpTheorems := relevantLemmas)
         (congrTheorems := ← getSimpCongrTheorems)
       let ⟨result?, _⟩ ←