Theorem: getBitResLast_symm_apply (Controlbits/BitResiduum.lean)

State before:
b : Bool
a✝ : ℕ
p : BV a✝
⊢ getBitResZero.symm (b, p) = finProdFinEquiv (p, bif b then 1 else 0)
Tactic:
cases b <;> rfl
State after:
no goals