Theorem: bitInvarMulEquiv_last_apply_condFlipBits (Controlbits/BitResiduum.lean)

State before:
m : ℕ
c : BV (m + 1) → Bool
i : Fin (m + 1)
⊢ ↑((bitInvarMulEquiv (Fin.last (m + 1))) fun b => condFlipBit i fun p => c (mergeBitRes (Fin.last m) b p)) =
    condFlipBit i.castSucc c
Tactic:
rw [← Fin.predAbove_right_last (i := i), bitInvarMulEquiv_apply_condFlipBits, Fin.succAbove_last]
State after:
no goals