Theorem: endoOfBoolArrowEndo_bitInvar (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
⊢ bitInvar i (endoOfBoolArrowEndo i f)
Tactic:
simp_rw [bitInvar_iff_getBit_apply_eq_getBit, endoOfBoolArrowEndo_def,
  getBit_mergeBitRes, implies_true]
State after:
no goals