Theorem: mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
f : Function.End (BV (a✝ + 1))
b : Bool
p : BV a✝
h : bitInvar i f
⊢ mergeBitRes i b (getRes i (f (mergeBitRes i b p))) = f (mergeBitRes i b p)
Tactic:
convert (getBit_mergeBitRes ▸ mergeBitRes_getBit_getRes_apply_eq_apply_of_bitinvar h)
State after:
no goals