Theorem: condFlipBit_mul_cancel_left (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c : BV a✝ → Bool
ρ : Equiv.Perm (BV (a✝ + 1))
⊢ condFlipBit i c * (condFlipBit i c * ρ) = ρ
Tactic:
rw [← mul_assoc, condFlipBit_mul_self, one_mul]
State after:
no goals