rw [this]
α : 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
α : 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
⊢ (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 =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x