Theorem: getBit_apply_two_pow (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ getBit i ⟨2 ^ ↑i, ⋯⟩ = true
Tactic:
rw [getBit_apply, getBitRes_apply_two_pow]
State after:
no goals