dsimp [Nat.fold]
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) Nat.zero (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) Nat.zero x, y <<< OfNat.ofNat Nat.zero)
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ (x, y) = (x, y <<< OfNat.ofNat 0)