suffices ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = i.getBit k by
  have what_is_shown :=
    this (Nat.log2RU $ length α) (Nat.log2RU_lt_self _ ‹0 < length α›)
  apply Nat.bitext; intro k
  cases Nat.lt_or_ge k (Nat.log2RU $ length α)
  case a.inl hlt => exact what_is_shown k hlt
  case a.inr hge =>
    unfold UInt.getBit at foldf_high; rw [foldf_high _ _ hge]
    suffices Nat.getBit i k = false
      from Eq.symm this
    apply Nat.getBit_high ?_ k hge
    calc
      i < length α := ‹_›
      _ ≤ 2^Nat.log2RU (length α) := Nat.le_pow2_log2RU_self _
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
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
⊢ ∀ (n : Nat), n < length α → ∀ (k : Nat), k < n → UInt.getBit (Nat.fold f n 0) k = Nat.getBit i k