Theorem: flipBit_mul_self (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ flipBit i * flipBit i = 1
Tactic:
rw [mul_eq_one_iff_inv_eq]
State after:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ (flipBit i)⁻¹ = flipBit i

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
⊢ (flipBit i)⁻¹ = flipBit i
Tactic:
exact flipBit_inv
State after:
no goals