∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {H : Type u_1} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H],
  Function.RightInverse (fun e => ⟨↑e.toContinuousLinearEquiv, ⋯⟩) fun u =>
    let __src := ↑u;
    { toLinearMap := ↑__src, invFun := ⇑↑↑(star u), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }