Theorem: endoOfBoolArrowEndo_leftInverse_apply (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f g : Bool → Function.End (BV m)
hfg : ∀ (b : Bool), Function.LeftInverse (f b) (g b)
q : BV (m + 1)
⊢ endoOfBoolArrowEndo i f (endoOfBoolArrowEndo i g q) = q
Tactic:
simp_rw [endoOfBoolArrowEndo_def, getBit_mergeBitRes, getRes_mergeBitRes,
  hfg (getBit i q) (getRes i q), mergeBitRes_getBit_getRes]
State after:
no goals