Theorem: bitInvar_comp_of_bitInvar (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
f g : Function.End (BV (a✝ + 1))
hf : bitInvar i f
hg : bitInvar i g
q : BV (a✝ + 1)
⊢ getBit i ((f ∘ g) q) = getBit i q
Tactic:
simp_rw [Function.comp_apply, hf (g q), hg q]
State after:
no goals