Theorem: endoOfBoolArrowEndo_leftInvOn (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
f : Function.End (BV (m + 1))
hf : f ∈ bitInvar i
⊢ endoOfBoolArrowEndo i (boolArrowEndoOfEndo i f) = f
Tactic:
ext q
State after:
case H.h
m : ℕ
i : Fin (m + 1)
f : Function.End (BV (m + 1))
hf : f ∈ bitInvar i
q : BV (m + 1)
⊢ ↑(endoOfBoolArrowEndo i (boolArrowEndoOfEndo i f) q) = ↑(f q)

State before:
case H.h
m : ℕ
i : Fin (m + 1)
f : Function.End (BV (m + 1))
hf : f ∈ bitInvar i
q : BV (m + 1)
⊢ ↑(endoOfBoolArrowEndo i (boolArrowEndoOfEndo i f) q) = ↑(f q)
Tactic:
simp_rw [endoOfBoolArrowEndo_def, boolArrowEndoOfEndo_def, mergeBitRes_getBit_getRes,
mergeBitRes_getRes_of_getBit_eq (hf q)]
State after:
no goals