dsimp
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (match (x, 1) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> k, k <<< 1)) =
    match (x, 1) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
        1 <<< OfNat.ofNat (0 + 1))
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> 1, 1 <<< 1) =
    ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
      1 <<< OfNat.ofNat (0 + 1))