Could Pre-image theorem be generalized to Hilbert Manifolds?

Question

$f:M\to N$ is a smooth map between manifolds of dimensions $m\geq n$. If $y\in N$ is a regular value, then the set $f^{-1}(y)$ is a smooth manifold of dimension $m-n$ or $\emptyset$.

Could the Pre-image theorem be generalized to Hilbert space or other infinite dimensional spaces?

Answer 1

Corollary 5.8 (page 17) in "Introduction to Differentiable Manifolds" by S.Lang. You do not even need Banach manifolds for this, just manifolds modeled on topological vector spaces. This corollary implies that each regular level set $f^{-1}(y)$ is a smooth submanifold of the same codimension as the dimension of the target manifold.