feat: USize.and_toNat (#4629)

Split from #4583

src/Init/Data/Fin/Bitwise.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.Nat.Bitwise
+import Init.Data.Fin.Basic
+
+namespace Fin
+
+@[simp] theorem and_val (a b : Fin n) : (a &&& b).val = a.val &&& b.val :=
+  Nat.mod_eq_of_lt (Nat.lt_of_le_of_lt Nat.and_le_left a.isLt)
+
+end Fin

src/Init/Data/UInt.lean

@@ -7,3 +7,4 @@ prelude
 import Init.Data.UInt.Basic
 import Init.Data.UInt.Log2
 import Init.Data.UInt.Lemmas
+import Init.Data.UInt.Bitwise

src/Init/Data/UInt/Bitwise.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+prelude
+import Init.Data.UInt.Basic
+import Init.Data.Fin.Bitwise
+
+set_option hygiene false in
+macro "declare_bitwise_uint_theorems" typeName:ident : command =>
+`(
+namespace $typeName
+
+@[simp] protected theorem and_toNat (a b : $typeName) : (a &&& b).toNat = a.toNat &&& b.toNat := Fin.and_val ..
+
+end $typeName
+)
+
+declare_bitwise_uint_theorems UInt8
+declare_bitwise_uint_theorems UInt16
+declare_bitwise_uint_theorems UInt32
+declare_bitwise_uint_theorems UInt64
+declare_bitwise_uint_theorems USize