Theorem: mergeBitRes_apply_true_zero (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ mergeBitRes i true 0 = ⟨2 ^ ↑i, ⋯⟩
Tactic:
rw [mergeBitRes_apply, ← getBitRes_apply_two_pow (i := i), Equiv.symm_apply_apply]
State after:
no goals