I have two real and separable Hilbert spaces $X$ and $Y$ as well as a continuously Fréchet differentiable function $f : X \to Y$ that is bijective. Furthermore, at every point $x \in X$, $D_x f \in \mathcal{L} \left( X, Y \right)$ is continuous, injective and has dense range. Now, I would love to throw some version of the inverse function theorem on this object to conclude that $f^{-1}$ is (at least) Gâteaux differentiable at every $y \in Y$ in all directions in the range of $D_{f^{-1} \left(y \right)} f$ in order to conclude that \begin{equation} D_y f^{-1} = \left( D_{f^{-1} \left(y \right)} f \right)^{-1} \end{equation} but I seem to be unable to find any such theorem or proving it myself.
I am looking for a compilation of inverse function theorems with different assumptions in order to see if I can prove that $f$ perhaps has another nice property allowing me to draw the above conclusion.
Note: I do not expect that $f^{-1}$ is continuous, at least so far I have been unable to prove it.
Under those assumptions, the Gateaux derivative of $f^{-1}$ might not exist. We cannot replace invertibility of the derivative by the weaker assumption of dense range. All the other assumptions do not make up for this. Here is a somewhat lengthy counterexample.
Take $X$ infinite-dimensional, $X=Y$. Let $K\in \mathcal L(X,X)$ be compact, injective, with dense range, self-adjoint, and positive semidefinite. Such operators exist. The idea is to build $f$ such that $f'(0)=K$.
For $y\in X$ define $$ F(x):=\frac12 \langle Kx,x\rangle + \frac13 \|x\|^3 - \langle x,y\rangle. $$ Due to the assumptions, $F$ is strictly convex, coercive, continuous. Hence $F$ has a uniquely defined global minimum, which is the only solution to $F'(x)=0$. Hence the equation $$ Kx + \|x\|^2 x = y $$ is uniquely solvable for all $y$. Set $$ f(x):=Kx + \|x\|^2 x. $$ Its derivative is given by $$ f'(x) = K + 2\langle x, \cdot\rangle x + \|x\|^2 Id, $$ which is positive definite and bijective for all $x\ne0$, injective with dense range for $x=0$.
Now let $y \in X\setminus R(K)$, which exists due to the assumptions on $K$. Let $x_t$ be defined as $f(x_t)=ty$. Then the difference quotient $\frac{x_t-0}t=\frac{f^{-1}(ty)-f^{-1}(0)}t$ does not converge for $t\searrow0$, and $f^{-1}$ is not even directionally differentiable at $y=0$. To see this, lets have a look on the equation defining $x_t$: $$ Kx_t + \|x_t\|^2 x_t =ty. $$ Divide this by $t$ and write it as an equation in $z_t:=t^{-1}x_t$: $$ Kz_t + t^2\|z_t\|^2 z_t =y. $$ If $z_t \to z$ then passing to the limit $t\searrow0$ in this equation gives $Kz=y$, which is impossible.