Theorem: boolArrowEndoOfEndo_mul_ofBitInvarRight (Controlbits/BitResiduum.lean)

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

State before:
case h
m : ℕ
i : Fin (m + 1)
f g : Function.End (BV (m + 1))
hg : bitInvar i g
x✝ : Bool
⊢ boolArrowEndoOfEndo i (f * g) x✝ = (boolArrowEndoOfEndo i f * boolArrowEndoOfEndo i g) x✝
Tactic:
exact boolArrowEndoOfEndo_comp_ofBitInvarRight hg
State after:
no goals