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