have foldf_high : ∀ (n k : Nat), k ≥ n → UInt.getBit (Nat.fold f n 0) k = false := by
  intro n k hnk
  induction n generalizing k
  case zero => dsimp [Nat.fold]; exact UInt.getBit_zero k
  case succ n h_ind =>
    dsimp [Nat.fold]
    rw [UInt.getBit_lor, h_ind k (Nat.le_of_succ_le hnk), Bool.or_false]
    cases decide (x &&& bitmask (OfNat.ofNat n) ≠ 0)
    case true =>
      rw [UInt.when_true_eq, UInt.getBit_shiftLeft]
      have : UInt.getBit (1 : α) (k - toNat (OfNat.ofNat (α:=α) n) % length α) = false := by
        rw [UInt.toNat_ofNat]
        have := calc
          n % 2^length α % length α
            ≤ n % 2^length α := Nat.mod_le ..
          _ ≤ n := Nat.mod_le ..
          _ < n.succ := n.lt_succ_self
          _ ≤ k := hnk
        have : k - n % 2^length α % length α > 0 :=
          Nat.lt_sub_of_add_lt (Nat.zero_add .. ▸ this)
        rw [UInt.getBit_one, decide_eq_false (Nat.ne_of_gt this), Bool.and_false]
      simp only [this, Bool.and_false]
    case false =>
      exact UInt.when_false_eq (α:=α) .. ▸ UInt.getBit_zero (α:=α) k
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
this✝¹ : UInt.getBit x i = true
this✝ : i < length α
this : 0 < length α
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i
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
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
⊢ toNat (Nat.fold f (Nat.log2RU (length α)) 0) = i