Theorem: getBit_base (Controlbits/BitResiduum.lean)

State before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getBit i q = decide (q = 1)
Tactic:
rw [Fin.eq_zero i]
State after:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getBit 0 q = decide (q = 1)

State before:
i : Fin (0 + 1)
q : BV (0 + 1)
⊢ getBit 0 q = decide (q = 1)
Tactic:
rcases Fin.exists_fin_two.mp ⟨q, rfl⟩ with (rfl | rfl) <;> rfl
State after:
no goals