Theorem: mergeBitRes_zero (Controlbits/BitResiduum.lean)

State before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ mergeBitRes 0 b p = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
simp_rw [mergeBitRes_apply, getBitRes_zero_symm_apply]
State after:
no goals