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

@@ -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
 

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