Looks good. Some comments:
I think you need to say like $N$ is a smooth (regular/embedded) submanifold because $N$ is an open submanifold because $N$ is open because $f$ is open because $f$ is a local diffeomorphism. This is the way $N$ is a smooth manifold by itself. I mean if you just have $N$ as immersed submanifold, then what would $f: X \to N$ even mean?
The way that $N$ is a smooth manifold in (1) preceding is relevant for (3) as follows.
Proving $f: X \to N$ I think is a wheel reinvention. Surely there should be some rule in the book that says restriction of range of a smooth map to any submanifold of range that contains image is also smooth (or at least that restriction of range to image is smooth).
A shortcut to showing $f^{-1}: N \to X$ is smooth: This is true if and only if $f$ is an immersion. See here. (I think also true if and only if $f$ is a submersion. See here.) Finally, local diffeomorphism at $p \in X$ is equivalent to both-immersion at $p$-and-submersion at $p$
Actually, you can prove something stronger.
This says: Injective local diffeomorphism only if (smooth) embedding.
So what condition on embedding allows to have an if? Open. Actually:
Injective local diffeomorphism if and only if open embedding. I ask and answer here: Is open (topological) smooth embedding equivalent to injective local (homeomorphism) diffeomorphism?
You can also observe and then ask other things:
Injective local diffeomorphism only if open immersion. So what condition on open immersion allows to have an if? Topological embedding.
Open embedding only if local diffeomorphism. So what condition on local diffeomorphism allows us to have an if? Injective.
I thought exactly the same and I think I've found a satisfactory solution. Basically your po\text{int } 1. is right, but the argument is indeed quite subtle.
I'm gonna divide this proof in 4 parts:
Part 1: If $M$ is a nonempty manifold with boundary then $\text{int }(M)\neq \emptyset$.
Proof: I'll leave this one as homework :) because it's not subtle.
Part 2: If $M\to N$ are nonempty diffeomorphic smooth manifolds with boundary with dimensions $m$ and $n$ then $m=n$.
Proof: This part is subtle, so I'll write the details carefully. Let $f:M\to N$ be a diffeomorphism. Then $f|\text{int } M:\text{int } M\to f(\text{int } M)$ is a diffeomorphism where $\text{int } M$ is a nonempty smooth manifold (this is because of part 1.) and $f(\text{int } M)$ is a nonempty smooth manifold with boundary. Let's rename $f|\text{int } M:\text{int } M\to f(\text{int } M)$ as $f_1:M_1\to N_1$. Using the same trick $f_1|f_1^{-1}(\text{int } N_1):f_1^{-1}(\text{int } N_1)\to \text{int } N_1$ is a diffeomorphism between nonempty smooth manifolds. By Proposition 2.17 (Diffeomorphism Invariance of Dimension) we have that $f_1^{-1}(\text{int } N_1)$ and $\text{int } N_1$ have the same dimension, so the same is true for $M$ and $N$.
Part 3: If $M$ is a smooth manifold with boundary, $(U,\phi)$ is a smooth chart for $M$ and $f:\phi(U)\to V$ is a diffeomorphism between open subsets of $\mathbb{H}^n$ or $\mathbb{R}^n$ then $(U,f\circ \phi)$ is a smooth chart for $M$.
Proof: I'll also leave this one for homework because it's also not subtle.
Part 4: (Theorem 2.18, Diffeomorphism Invariance of the Boundary): Suppose $M$ and $N$ are smooth manifolds with boundary and $F:M\to N$ is a diffeomorphism. Then $F(\partial M)=\partial N$.
Proof: Let $p\in \partial M$. This means there is a smooth chart $(U,\phi)$ for $M$ such that $p\in U$, $\phi(U)\subseteq \mathbb{H}^n$ and $\phi(U)\in \partial \mathbb{H}^n$. By restricting $U$ (this is essentially what Lee does in his proof of Theorem 2.17, Diffeomorphism Invariance of Dimension) we may find a chart $(F(U),\psi)$ for $N$. Then $\psi\circ F\circ \phi^{-1}:\phi(U)\to \psi(F(U))$ is a diffeomorphism between open subsets of the same $\mathbb{H}^n$ or $\mathbb{R}^n$ because of part 2. Define $\hat{F}=\psi\circ F\circ \phi^{-1}$, then by part 3. $(U,\hat{F}\circ \phi)$ is a smooth chart for $M$.
By Theorem 1.46 (Smooth Invariance of the Boundary) $\hat{F}(\phi(U))\subseteq \mathbb{H}^n$ and $\hat{F}(\phi(p))\in \partial \mathbb{H}^n$, this is the same as saying $\psi(F(U))\subseteq \mathbb{H}^n$ and $\psi(F(p))\in \partial \mathbb{H}^n$, which implies $F(p)\in \partial N$. So $F(\partial M)\subseteq \partial N$ and we are done.
This is the kind of details that always drives me crazy, but hopefully now I can fill most of the gaps. When I ask people about this kind of details I sometimes get offtopic answers by people that think this is a trivial detail. For example, I don't see how connectedness plays a role here, care to explain @Ted Shifrin?
Best Answer
To say that $f\colon M\to N$ is a local diffeomorphism means that each point of $M$ has an open neighborhood $U$ such that $f(U)$ is open in $N$ and $f|_U$ is a diffeomorphism from $U$ onto $f(U)$.
Theorem. If $M$ and $N$ are smooth manifolds with boundary and $f\colon M\to N$ is a local diffeomorphism, then $f(\partial M)\subseteq \partial N$.
Proof. Assume for contradiction that there is a point $p\in \partial M$ such that $f(p)\in \operatorname{Int} M$. Let $U$ and $V$ be open neighborhoods of $p$ and $f(p)$ respectively, such that $f|_U\colon U\to V$ is a diffeomorphism.
Because $p\in\partial M$, there is a vector $v\in T_pM$ that is not tangent to $\partial M$. This means, in particular, that there is no smooth curve $\gamma\colon (-\varepsilon,\varepsilon)\to M$ such that $\gamma(0)=p$ and $\gamma'(0)=v$. Let $w = df_p(v) \in T_{f(p)}N$. Because $f(p)$ is an interior point of $N$, there is a smooth curve $\gamma\colon (-\varepsilon,\varepsilon)\to V$ such that $\gamma(0) = f(p)$ and $\gamma'(0) = w$. Then $\tilde\gamma = f^{-1}\circ \gamma$ is a smooth curve in $M$ such that $\tilde\gamma(0)=p$ and $\tilde\gamma'(0) = v$, which is a contradiction. $\square$
When $M$ and $N$ both have empty boundaries (and the same dimension), it's easy to show using the inverse function theorem that a smooth map $f\colon M\to N$ is a local diffeomorphism if and only if it is an immersion (a map whose differential is injective at each point). But in the case of nonempty boundaries, this isn't true. There are plenty of examples (such as those described by Andrew Hwang) of smooth immersions that take boundary points to interior points, but they're not local diffeomorphisms.