From 0dc317c73c8ded4fabb348116186f43f2488e9e3 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 28 Aug 2024 12:38:57 +1000
Subject: [PATCH] feat: restore reduceCtorEq in norm_cast tactic (#5187)

#5167 removed `reduceCtorEq` from the default simproc set. `norm_cast`
relies on it, so we add it back in there.
---
 src/Lean/Elab/Tactic/NormCast.lean | 4 +++-
 tests/lean/run/norm_cast.lean      | 3 +++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean
index aaf5373ca71b..e4e13c379c93 100644
--- a/src/Lean/Elab/Tactic/NormCast.lean
+++ b/src/Lean/Elab/Tactic/NormCast.lean
@@ -198,10 +198,12 @@ def derive (e : Expr) : MetaM Simp.Result := do
     let post := upwardAndElim (← normCastExt.up.getTheorems)
     r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
 
+  let simprocs ← ({} : Simp.SimprocsArray).add `reduceCtorEq false
+
   -- step 3: casts are squashed
   let r ← withTrace "squashing" do
     let simpTheorems := #[← normCastExt.squash.getTheorems]
-    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems }).1
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems } simprocs).1
 
   return r
 
diff --git a/tests/lean/run/norm_cast.lean b/tests/lean/run/norm_cast.lean
index 51d792b39b20..56e2b2be3991 100644
--- a/tests/lean/run/norm_cast.lean
+++ b/tests/lean/run/norm_cast.lean
@@ -82,3 +82,6 @@ theorem b (_h g : true) : true ∧ true := by
   constructor
   assumption_mod_cast
   assumption_mod_cast
+
+example : ¬n - k + 1 = 0 := by
+  norm_cast