We all know the "open mapping" part of the inverse function theorem on Euclidean spaces can be proved by either contraction mapping (iterations), or homotopy methods (degree theory / algebraic topology etc.). Yet the inverse function theorem on Banach spaces can only be proved by iteration methods, and homotopy methods fail, mostly due to Kuiper's theorem.

My question is: **is there any proof of the inverse function theorem on Banach spaces that does not use iteration methods**? It's sad to think the homotopy methods are a geometric coincidence of finite-dimensional spaces. The closest thing I know that could extend the homotopy methods would be Leray-Schauder degree theory, but that is restricted to maps of the form $\mathrm{Id}-K$ where $K$ is a continuous map that maps the unit ball to a precompact set (essentially close to being finite-dimensional). We would need something else to handle general $C^1$ maps.

I am interested in this problem because there are questions in PDE, related in spirit to the inverse function theorem, where finding the right iteration methods can be very difficult. Though I don't have much hope that anyone has figured out a way past the limitations of Leray-Schauder, I just want to put this question out there to let people know about the problem and maybe share some thoughts.