feat(data/nat/bitwise): test bits of powers of two (#6070)

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

src/data/nat/bitwise.lean

@@ -104,6 +104,29 @@ begin
     linarith }
 end
 
+@[simp]
+lemma test_bit_two_pow_self (n : ℕ) : test_bit (2 ^ n) n = tt :=
+by rw [test_bit, shiftr_eq_div_pow, nat.div_self (pow_pos zero_lt_two n), bodd_one]
+
+lemma test_bit_two_pow_of_ne {n m : ℕ} (hm : n ≠ m) : test_bit (2 ^ n) m = ff :=
+begin
+  rw [test_bit, shiftr_eq_div_pow],
+  cases hm.lt_or_lt with hm hm,
+  { rw [nat.div_eq_zero, bodd_zero],
+    exact nat.pow_lt_pow_of_lt_right one_lt_two hm },
+  { rw [pow_div hm.le zero_lt_two, ←nat.sub_add_cancel (nat.sub_pos_of_lt hm), pow_succ],
+    simp }
+end
+
+lemma test_bit_two_pow (n m : ℕ) : test_bit (2 ^ n) m = (n = m) :=
+begin
+  by_cases n = m,
+  { cases h,
+    simp },
+  { rw test_bit_two_pow_of_ne h,
+    simp [h] }
+end
+
 /-- If `f` is a commutative operation on bools such that `f ff ff = ff`, then `bitwise f` is also
     commutative. -/
 lemma bitwise_comm {f : bool → bool → bool} (hf : ∀ b b', f b b' = f b' b)