Theorem: boolArrowEndoOfEndo_rightInverse_apply_ofBitInvarLeft (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hfg : Function.RightInverse f g
hf : bitInvar i f
b : Bool
q : BV m
⊢ boolArrowEndoOfEndo i g b (boolArrowEndoOfEndo i f b q) = q
Tactic:
simp_rw [boolArrowEndoOfEndo_def, mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar hf,
hfg (mergeBitRes i b q), getRes_mergeBitRes]
State after:
no goals