Lemmas about Nat.testBit and bitwise folds

Statements that mention nothing from this development. They were proved here because something in the library needed them, and they are collected in ForMathlib so that they can be contributed upstream, or deleted when Mathlib grows its own.

theorem eq_of_testBit_lt {n a b : ℕ} (ha : a < 2 ^ n) (hb : b < 2 ^ n) (h : ∀ k < n, a.testBit k = b.testBit k) : a = b

theorem testBit_foldl_or {α : Type} (f : α → ℕ) (p : α → Bool) (k : ℕ) (l : List α) (c : ℕ) : (List.foldl (fun (c : ℕ) (a : α) => if p a = true then c ||| 2 ^ f a else c) c l).testBit k = (c.testBit k || l.any fun (a : α) => p a && decide (f a = k))

theorem foldl_or_lt {α : Type} (f : α → ℕ) (p : α → Bool) (m : ℕ) (l : List α) (hf : ∀ a ∈ l, f a < m) (c : ℕ) (hc : c < 2 ^ m) : List.foldl (fun (c : ℕ) (a : α) => if p a = true then c ||| 2 ^ f a else c) c l < 2 ^ m

theorem exists_testBit {n s : ℕ} (hs : s < 2 ^ n) (h0 : s ≠ 0) : ∃ (i : Fin n), s.testBit ↑i = true

theorem le_of_testBit_imp {a b : ℕ} (h : ∀ (k : ℕ), a.testBit k = true → b.testBit k = true) : a ≤ b

theorem testBit_foldl_lor {α : Type} (f : α → ℕ) (p : α → Bool) (k : ℕ) (l : List α) (c : ℕ) : (List.foldl (fun (c : ℕ) (a : α) => if p a = true then c ||| f a else c) c l).testBit k = (c.testBit k || l.any fun (a : α) => p a && (f a).testBit k)

theorem shl_bit (acc : UInt64) (c : Bool) (t : ℕ) (ht : t < 64) : (acc <<< 1 ||| if c = true then 1 else 0).toBitVec.getLsbD t = if t = 0 then c else acc.toBitVec.getLsbD (t - 1)

theorem shl_natshift (acc : UInt64) (m : ℕ) (hm : m < 64) : (acc <<< UInt64.ofNat m).toBitVec = acc.toBitVec <<< m