diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
index d06e1ad32caa..33ee83ecba22 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
@@ -49,17 +49,13 @@ If they do, they must disable the following `simprocs`.
 -/
 
 builtin_dsimproc [simp, seval] reduceNeg ((- _ : Int)) := fun e => do
-  unless e.isAppOfArity ``Neg.neg 3 do return .continue
-  let arg := e.appArg!
+  let_expr Neg.neg _ _ arg ← e | return .continue
   if arg.isAppOfArity ``OfNat.ofNat 3 then
     -- We return .done to ensure `Neg.neg` is not unfolded even when `ground := true`.
     return .done e
   else
     let some v ← fromExpr? arg | return .continue
-    if v < 0 then
-      return .done <| toExpr (- v)
-    else
-      return .done <| toExpr v
+    return .done <| toExpr (- v)
 
 /-- Return `.done` for positive Int values. We don't want to unfold in the symbolic evaluator. -/
 builtin_dsimproc [seval] isPosValue ((OfNat.ofNat _ : Int)) := fun e => do
diff --git a/tests/lean/run/6467.lean b/tests/lean/run/6467.lean
new file mode 100644
index 000000000000..f4d0a606b6b1
--- /dev/null
+++ b/tests/lean/run/6467.lean
@@ -0,0 +1,16 @@
+theorem confuses_the_user : -(no_index (OfNat.ofNat <| nat_lit 2)) = -2 := by
+  simp
+
+theorem ex : -(no_index (OfNat.ofNat <| nat_lit 2)) = (2 : Int) := by
+  simp only [Int.reduceNeg]
+  guard_target =ₛ -2 = 2
+  sorry
+
+theorem its_true_really : -(no_index (OfNat.ofNat <| nat_lit 2)) = -2 := by
+  rfl
+
+example : -(-(no_index (OfNat.ofNat <| nat_lit 2))) = 2 := by
+  simp
+
+example : -(no_index (-(no_index (OfNat.ofNat <| nat_lit 2)))) = -(-(-(-3+1))) := by
+  simp