Theorem: bitInvar_of_comp_bitInvar_bitInvar (Controlbits/BitResiduum.lean)

State before:
a✝ : ℕ
i : Fin (a✝ + 1)
f g : BV (a✝ + 1) → BV (a✝ + 1)
hfg : bitInvar i (f ∘ g)
h : bitInvar i f
q : BV (a✝ + 1)
⊢ getBit i (g q) = getBit i q
Tactic:
rw [← h (g q), ← hfg q, Function.comp_apply]
State after:
no goals