∀ (R : Type u_3) (A : Type u_2) (E : Type u_1) [inst : Semiring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E],
  Function.RightInverse (LinearEquiv.refl R (WithCStarModule A E)).invFun
    (↑(LinearEquiv.refl R (WithCStarModule A E))).toFun