Theorem: condFlipBit_flipBit_of_all_true (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ flipBit i = condFlipBit i (Function.const (BV a✝) true)
Tactic:
ext
State after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑((condFlipBit i (Function.const (BV a✝) true)) x✝)

State before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑((condFlipBit i (Function.const (BV a✝) true)) x✝)
Tactic:
rw [condFlipBit_apply]
State after:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑(bif Function.const (BV a✝) true (getRes i x✝) then (flipBit i) x✝ else x✝)

State before:
case H.h
a✝ : ℕ
i : Fin (a✝ + 1)
x✝ : BV (a✝ + 1)
⊢ ↑((flipBit i) x✝) = ↑(bif Function.const (BV a✝) true (getRes i x✝) then (flipBit i) x✝ else x✝)
Tactic:
rfl
State after:
no goals