Theorem: condFlipBitCore_condFlipBitCore (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
q : BV (a✝ + 1)
⊢ condFlipBitCore i c (condFlipBitCore i c q) = q
Tactic:
rcases (c (getRes i q)).dichotomy with h | h <;>
simp only [condFlipBitCore, h, cond_true, cond_false, getRes_flipBit, flipBit_flipBit]
State after:
no goals