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