case succ =>
  intro i a h; cases a with | mk x k =>
  dsimp
  apply congrArg (Prod.mk _)
  rw [UInt.shiftLeft_shiftLeft 1 (OfNat.ofNat (i+1)) 1, UInt.ofNat_add]
  . simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
    have : length α > 0 :=
      hn |> (length α).rec (λ (hn : 0 = n) => nomatch (trans h hn.symm)) (λ l _ _ => l.zero_lt_succ)
    have : n < length α := hn ▸ Nat.log2RU_lt_self _ ‹length α > 0›
    have : n < 2^length α := trans this (Nat.exp_lt_pow (length α) .refl)
    rw [
        Nat.mod_eq_of_lt (trans h this),
        Nat.mod_eq_of_lt (trans (trans (Nat.le_add_left 1 i) h) this)
    ]
    exact trans (r:=LE.le) (h : i+2 ≤ n) ‹n < length α›
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i + 1 < n →
      (match
          match a 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 a 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))
no goals