Theorem: mergeBitRes_getBit_getRes_apply_eq_apply_of_bitinvar (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
f : Function.End (BV (a✝ + 1))
q : BV (a✝ + 1)
h : bitInvar i f
⊢ mergeBitRes i (getBit i q) (getRes i (f q)) = f q
Tactic:
rw [← h q, mergeBitRes_getBit_getRes]
State after:
no goals