unfold UInt.getBit at foldf_high
α : 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
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k
α : 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
this✝² : UInt.getBit x i = true
this✝¹ : i < length α
this✝ : 0 < length α
foldf_high : ∀ (n k : Nat), k ≥ n → Nat.getBit (toNat (Nat.fold f n 0)) k = false
this : ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k
what_is_shown :
  ∀ (k : Nat), k < Nat.log2RU (length α) → UInt.getBit (Nat.fold f (Nat.log2RU (length α)) 0) k = Nat.getBit i k
k : Nat
hge : k ≥ Nat.log2RU (length α)
⊢ Nat.getBit (toNat (Nat.fold f (Nat.log2RU (length α)) 0)) k = Nat.getBit i k