conv =>
  rhs; dsimp
α : 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
α : 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 (fun n x => UInt.when (decide ¬a &&& bitmask (OfNat.ofNat n) = 0) (1 <<< OfNat.ofNat n) ||| x)
      (Nat.log2RU (length α)) x