Theorem: mergeBitRes_getBit_getRes (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
⊢ mergeBitRes i (getBit i q) (getRes i q) = q
Tactic:
simp_rw [getRes_apply, mergeBitRes_apply, getBit_apply, Prod.mk.eta, Equiv.symm_apply_apply]
State after:
no goals