have : bitcnt x = (Prod.fst $ (x,1) |> Fin.foldAll λ (i : Fin (Nat.log2RU (length α))) ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i.1)) + ((x &&& bitmask (OfNat.ofNat i.1)) >>> k), k <<< 1)) := by
  unfold bitcnt; unfold maskTable
  simp only [Array.foldl_ofFn_eq]; rfl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
this :
  bitcnt x =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
⊢ bitcnt x =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x