Reference request: Variations of inverse function theorem 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.
 A: 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.
