suffices ∀ (a x : α), (maskTable.foldl (f a) (x,1)).1 = Nat.fold (f' a) (Nat.log2RU $ length α) x
  from λ a => this (UInt.lsb a) ..
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a : α), UInt.ctz a = UInt.ctz' a
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
f : α → α × α → α → α × α := fun a₁ z m => (UInt.when (decide (a₁ &&& m ≠ 0)) z.snd ||| z.fst, z.snd <<< 1)
f' : α → Nat → α → α :=
  fun a₁ n x => UInt.when (decide (a₁ &&& bitmask (OfNat.ofNat n) ≠ 0)) (1 <<< OfNat.ofNat n) ||| x
⊢ ∀ (a x : α),
    (Array.foldl (f a) (x, 1) maskTable 0 (Array.size maskTable)).fst = Nat.fold (f' a) (Nat.log2RU (length α)) x