Theorem: boolArrowEndoOfEndo_leftInverse_apply_ofBitInvarLeft (Controlbits/BitResiduum.lean)

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