Theorem: flipBit_base (Controlbits/BitResiduum.lean)

State before:
i : Fin (0 + 1)
⊢ flipBit i = Equiv.swap 0 1
Tactic:
simp_rw [Equiv.ext_iff, flipBit_apply, Fin.eq_zero i]
State after:
i : Fin (0 + 1)
⊢ ∀ (x : BV (0 + 1)), mergeBitRes 0 (!getBit 0 x) (getRes 0 x) = (Equiv.swap 0 1) x

State before:
i : Fin (0 + 1)
⊢ ∀ (x : BV (0 + 1)), mergeBitRes 0 (!getBit 0 x) (getRes 0 x) = (Equiv.swap 0 1) x
Tactic:
exact Fin.forall_fin_two.mpr ⟨rfl, rfl⟩
State after:
no goals