Theorem: endoOfBoolArrowEndo_comp (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f g : Bool → Function.End (BV m)
⊢ (endoOfBoolArrowEndo i fun b => f b ∘ g b) = endoOfBoolArrowEndo i f ∘ endoOfBoolArrowEndo i g
Tactic:
simp_rw [Function.End.ext_iff, Function.comp_apply, endoOfBoolArrowEndo_def,  getBit_mergeBitRes,
getRes_mergeBitRes, Function.comp_apply, implies_true]
State after:
no goals