diff --git a/src/Lean/Elab/Tactic/NormCast.lean b/src/Lean/Elab/Tactic/NormCast.lean
index aaf5373ca7..e4e13c379c 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 51d792b39b..56e2b2be39 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