Theorem: boolArrowEndoOfEndo_comp_ofBitInvarRight (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
b : Bool
⊢ boolArrowEndoOfEndo i (f ∘ g) b = boolArrowEndoOfEndo i f b ∘ boolArrowEndoOfEndo i g b
Tactic:
ext
State after:
case H.h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
b : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (f ∘ g) b x✝) = ↑((boolArrowEndoOfEndo i f b ∘ boolArrowEndoOfEndo i g b) x✝)

State before:
case H.h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
b : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (f ∘ g) b x✝) = ↑((boolArrowEndoOfEndo i f b ∘ boolArrowEndoOfEndo i g b) x✝)
Tactic:
simp_rw [boolArrowEndoOfEndo_def, Function.comp_apply, boolArrowEndoOfEndo_def,
mergeBitRes_getRes_apply_mergeBitRes_of_bitinvar hg]
State after:
no goals