Theorem: getBit_condFlipBit'' (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ getBit i ((condFlipBit i c) q) = bif getBit i q then !c (getRes i q) else c (getRes i q)
Tactic:
rcases (getBit i q).dichotomy with hc | hc <;>
simp only [getBit_condFlipBit', hc, Bool.xor_false, Bool.xor_true, cond_true, cond_false]
State after:
no goals