diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index e6eb98c13b..edc24c29b6 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -664,3 +664,6 @@ but may be used locally.
 
 @[simp] theorem Bool.not'_eq_not (a : Bool) : a.not' = a.not := by
   cases a <;> simp [Bool.not']
+
+theorem Bool.rec_eq {α : Sort _} (b : Bool) {x y : α} : Bool.rec y x b = if b then x else y := by
+  cases b <;> simp
diff --git a/src/Init/Data/Nat/Bitwise/Basic.lean b/src/Init/Data/Nat/Bitwise/Basic.lean
index d5a19263f0..ad920d6cfe 100644
--- a/src/Init/Data/Nat/Bitwise/Basic.lean
+++ b/src/Init/Data/Nat/Bitwise/Basic.lean
@@ -102,6 +102,12 @@ instance : XorOp Nat := ⟨Nat.xor⟩
 instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
 instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
 
+@[simp] theorem land_eq {m n : Nat} : m.land n = m &&& n := rfl
+@[simp] theorem lor_eq {m n : Nat} : m.lor n = m ||| n := rfl
+@[simp] theorem xor_eq {m n : Nat} : m.xor n = m ^^^ n := rfl
+@[simp] theorem shiftLeft_eq' {m n : Nat} : m.shiftLeft n = m <<< n := rfl
+@[simp] theorem shiftRight_eq' {m n : Nat} : m.shiftRight n = m >>> n := rfl
+
 theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
   match b with
   | 0 => (Nat.mul_one _).symm