Theorem: condFlipBit_mul_self (Controlbits/BitResiduum.lean)

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

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