conv =>
  lhs; unfold maskTable; zeta; rw [Array.foldl_ofFn_eq]; dsimp [flip, Function.comp]
  change (Fin.foldAll ((λ (n : Nat) (z : α × α) => (UInt.when (a &&& bitmask (OfNat.ofNat (α:=α) n) ≠ 0) z.2 ||| z.1, z.2 <<< 1)) ∘ Fin.val (n:=Nat.log2RU $ length α)) (x, 1)).1
  rw [Fin.foldAll_comp_val]
α : 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
α : 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 : α
⊢ (Nat.fold (fun n z => (UInt.when (decide (a &&& bitmask (OfNat.ofNat n) ≠ 0)) z.snd ||| z.fst, z.snd <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (f' a) (Nat.log2RU (length α)) x