have : Nat.fold (λ i ((x,k) : α × α) => ((x &&& ~~~ bitmask (OfNat.ofNat i)) + ((x &&& bitmask (OfNat.ofNat i)) >>> k), k <<< 1)) n (x,1) = Nat.fold (λ i ((x,_) : α × α) => ((x &&& ~~~ bitmask (α:=α) (OfNat.ofNat i)) + ((x &&& bitmask (α:=α) (OfNat.ofNat i)) >>> ((1 : α) <<< OfNat.ofNat i)), (1 : α) <<< OfNat.ofNat (i+1))) n (x,1) := by
  apply Nat.fold_congr
  case zero => dsimp; rw [UInt.shiftLeft_zero]
  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
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
this :
  Nat.fold
      (fun i x =>
        match x with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
      n (x, 1) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x