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 c (getRes i q) then !getBit i q else getBit i q
Tactic:
rcases (c (getRes i q)).dichotomy with hc | hc <;>
simp only [condFlipBit_apply, cond_false, hc, cond_true, getBit_flipBit]
State after:
no goals