From e8bbba06b712dc6612a468c681245e0c642e6bce Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Sat, 25 Jan 2025 13:57:24 +0100
Subject: [PATCH] fix: fix builtin simproc `Nat.reduceAnd` (#6773)

This PR fixes a typo that prevented `Nat.reduceAnd` from working
correctly.

Closes #6772
---
 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 2 +-
 tests/lean/run/simprocNat.lean                     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index f3f9ac1e34..47651cd617 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -61,7 +61,7 @@ builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
   unless (← checkExponent m) do return .continue
   return .done <| toExpr (n ^ m)
 
-builtin_dsimproc [simp, seval] reduceAnd ((_ &&& _ : Nat)) := reduceBin ``HOr.hOr 6 (· &&& ·)
+builtin_dsimproc [simp, seval] reduceAnd ((_ &&& _ : Nat)) := reduceBin ``HAnd.hAnd 6 (· &&& ·)
 builtin_dsimproc [simp, seval] reduceXor ((_ ^^^ _ : Nat)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
 builtin_dsimproc [simp, seval] reduceOr ((_ ||| _ : Nat)) := reduceBin ``HOr.hOr 6 (· ||| ·)
 
diff --git a/tests/lean/run/simprocNat.lean b/tests/lean/run/simprocNat.lean
index 727497c0cb..a8da8a2a34 100644
--- a/tests/lean/run/simprocNat.lean
+++ b/tests/lean/run/simprocNat.lean
@@ -2,7 +2,7 @@ variable (a b : Nat)
 
 /- bitwise operation tests -/
 
-#check_simp (3 : Nat) &&& (1 : Nat) ~> 1
+#check_simp (4 : Nat) &&& (5 : Nat) ~> 4
 #check_simp (3 : Nat) ^^^ (1 : Nat) ~> 2
 #check_simp (2 : Nat) ||| (1 : Nat) ~> 3
 #check_simp (3 : Nat) <<< (2 : Nat) ~> 12