Theorem: mergeBitRes_inv (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
q : BV (a✝ + 1)
b : Bool
p : BV a✝
h₁ : getBit i q = b
h₂ : getRes i q = p
⊢ mergeBitRes i b p = q
Tactic:
simp_rw [← h₁, ← h₂, mergeBitRes_getBit_getRes]
State after:
no goals