Theorem: getBit_apply_zero_one (Controlbits/BitResiduum.lean)

State before:
m : ℕ
⊢ getBit 0 1 = true
Tactic:
convert getBit_apply_two_pow
State after:
case h.e'_2.h.e'_3.h.h.e'_2
m : ℕ
⊢ ↑1 = 2 ^ ↑0

State before:
case h.e'_2.h.e'_3.h.h.e'_2
m : ℕ
⊢ ↑1 = 2 ^ ↑0
Tactic:
rw [Fin.val_one', Nat.mod_eq_of_lt (Nat.one_lt_pow' _ _ ), Fin.val_zero, pow_zero]
State after:
no goals