theorem Nat.testBit_iff_mem_bitIndices (n i : ℕ) : n.testBit i = true ↔ i ∈ n.bitIndices

n.testBit i = true if and only if i appears in n.bitIndices. This connects the pointwise bit test with the list of set bit positions.

theorem Nat.testBit_finset_sum_pow_two {s : Finset ℕ} {i : ℕ} : (∑ x ∈ s, 2 ^ x).testBit i = true ↔ i ∈ s

Nat.testBit of a sum of distinct powers of 2 equals membership in the index set. For a finset s of natural numbers, (∑ i ∈ s, 2^i).testBit j = true ↔ j ∈ s.

theorem Nat.testBit_sum_pow_two_fin {k : ℕ} {s : Finset (Fin k)} (j : Fin k) : (∑ i ∈ s, 2 ^ ↑i).testBit ↑j = true ↔ j ∈ s

Nat.testBit of a sum of 2^j.val over Finset (Fin k) equals membership. This is the Fin-indexed version of Nat.testBit_finset_sum_pow_two.