Theorem: condFlipBit_base (Controlbits/BitResiduum.lean)

State before:
i : Fin (0 + 1)
c : BV 0 → Bool
⊢ condFlipBit i c = bif c 0 then Equiv.swap 0 1 else 1
Tactic:
ext q : 1
State after:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (condFlipBit i c) q = (bif c 0 then Equiv.swap 0 1 else 1) q

State before:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (condFlipBit i c) q = (bif c 0 then Equiv.swap 0 1 else 1) q
Tactic:
rw [condFlipBit_apply, Fin.eq_zero (getRes i q), flipBit_base]
State after:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (bif c 0 then (Equiv.swap 0 1) q else q) = (bif c 0 then Equiv.swap 0 1 else 1) q

State before:
case H
i : Fin (0 + 1)
c : BV 0 → Bool
q : BV (0 + 1)
⊢ (bif c 0 then (Equiv.swap 0 1) q else q) = (bif c 0 then Equiv.swap 0 1 else 1) q
Tactic:
cases (c 0) <;> rfl
State after:
no goals