if hlength : length α = 0
then exact UInt.eq_of_length_eq_zero hlength ..
else
have := this
  (f:=λ i x => UInt.when (a &&& bitmask (OfNat.ofNat i) ≠ 0) x)
  (n:=Nat.log2RU $ length α) (y:=1)
  (Nat.log2RU_lt_self (length α) (Nat.zero_lt_of_ne_zero hlength))
exact congrArg Prod.fst this
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
this :
  ∀ (f : Nat → α → α) (n : Nat) (y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
⊢ (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
no goals