Theorem: condFlipBit_comm (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
⊢ condFlipBit i c * condFlipBit i d = condFlipBit i d * condFlipBit i c
Tactic:
ext
State after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
x✝ : BV (a✝ + 1)
⊢ ↑((condFlipBit i c * condFlipBit i d) x✝) = ↑((condFlipBit i d * condFlipBit i c) x✝)

State before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
c d : BV a✝ → Bool
x✝ : BV (a✝ + 1)
⊢ ↑((condFlipBit i c * condFlipBit i d) x✝) = ↑((condFlipBit i d * condFlipBit i c) x✝)
Tactic:
simp_rw [Equiv.Perm.coe_mul, Function.comp_apply, condFlipBit_apply_comm]
State after:
no goals