Theorem: condFlipBit_apply_eq_swap_apply (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ (condFlipBit i c) q = (Equiv.swap q (mergeBitRes i (xor (c (getRes i q)) (getBit i q)) (getRes i q))) q
Tactic:
exact condFlipBit_apply_eq_mergeBitRes.trans (Equiv.swap_apply_left _ _).symm
State after:
no goals