conv =>
  change UInt.getBit x (toNat $ Nat.fold f (Nat.log2RU $ length α) 0) = true
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
⊢ UInt.getBit x
      (toNat
        (Nat.fold (fun n x_1 => UInt.when (decide ¬x &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x_1)
          (Nat.log2RU (length α)) 0)) =
    true
case intro
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
i : Nat
x : α
hi : ∀ (j : Nat), UInt.getBit x j = decide (i = j)
f : Nat → α → α := fun i y => UInt.when (decide (x &&& bitmask (OfNat.ofNat i) ≠ 0)) (1 <<< OfNat.ofNat i) ||| y
⊢ UInt.getBit x (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) = true