rw [toNat_ofNat (α:=α), Nat.mod_eq_of_lt ‹n < 2^length α›]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ (decide (i < length α) && Nat.getBit i (toNat (OfNat.ofNat n))) = (decide (i < length α) && Nat.getBit i n)
no goals