Theorem: mergeBitRes_getRes_of_getBit_not (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
b : Bool
h : getBit i q = !b
⊢ mergeBitRes i b (getRes i q) = (flipBit i) q
Tactic:
simp_rw [flipBit_apply, h, Bool.not_not]
State after:
no goals