Theorem: mergeBitRes_zero_apply_true_zero_eq_one (Controlbits/BitResiduum.lean)

State before:
m : ℕ
⊢ mergeBitRes 0 true 0 = 1
Tactic:
simp_rw [mergeBitRes_zero, Fin.ext_iff, finProdFinEquiv_apply_val, Fin.val_zero', mul_zero,
add_zero, Bool.cond_true, Fin.val_one, Fin.val_one', ← Nat.pow_succ,
Nat.mod_eq_of_lt (Nat.one_lt_pow' _ _ )]
State after:
no goals