Theorem: mergeBitRes_apply_false_zero (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ mergeBitRes i false 0 = 0
Tactic:
rw [mergeBitRes_apply, ← getBitRes_apply_zero (i := i), Equiv.symm_apply_apply]
State after:
no goals