Theorem: endoOfBoolArrowEndo_rightInverse (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
⊢ boolArrowEndoOfEndo i (endoOfBoolArrowEndo i f) = f
Tactic:
ext
State after:
case h.H.h
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
x✝¹ : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (endoOfBoolArrowEndo i f) x✝¹ x✝) = ↑(f x✝¹ x✝)

State before:
case h.H.h
m : ℕ
i : Fin (m + 1)
f : Bool → Function.End (BV m)
x✝¹ : Bool
x✝ : BV m
⊢ ↑(boolArrowEndoOfEndo i (endoOfBoolArrowEndo i f) x✝¹ x✝) = ↑(f x✝¹ x✝)
Tactic:
simp_rw [boolArrowEndoOfEndo_def, endoOfBoolArrowEndo_def, getBit_mergeBitRes,
getRes_mergeBitRes]
State after:
no goals