Theorem: getBitRes_zero_symm_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
b : Bool
p : BV m
⊢ (getBitRes 0).symm (b, p) = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
simp_rw [getBitRes_zero, getBitResZero_symm_apply]
State after:
no goals