have : (k >>> toNat n &&& 1) <<< k < 2^length α :=
  calc (k >>> toNat n &&& 1) <<< k
    _ = (k >>> toNat n &&& 1) * 2^k := Nat.shiftLeft_eq _ k
    _ ≤ 1*2^k := Nat.mul_le_mul_right _ $ by rw [Nat.land_one]; exact Nat.le_of_lt_succ (Nat.mod_lt _ (Nat.zero_lt_succ 1))
    _ = 2^k := Nat.one_mul _
    _ < 2^length α := Nat.pow_lt_pow_right Nat.le.refl hk
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝¹ : k < 2 ^ length α
this✝ : 2 ^ toNat n < 2 ^ length α
this : 1 < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != Nat.getBit ((k >>> toNat n &&& 1) <<< k % 2 ^ length α) i) = ?m.37836
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
k : Nat
h_ind : k ≤ length α → UInt.getBit (bitmask.aux n k) i = (decide (i < k) && Nat.getBit i (toNat n))
hk : Nat.succ k ≤ length α
this✝² : k < 2 ^ length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
this : (k >>> toNat n &&& 1) <<< k < 2 ^ length α
⊢ ((decide (i < k) && Nat.getBit i (toNat n)) != Nat.getBit ((k >>> toNat n &&& 1) <<< k % 2 ^ length α) i) = ?m.37836