[proofplan] We prove the inclusion by proving its contrapositive. If a covector is absent from $WF^t(u)$, the definition gives an elliptic microlocal cutoff $A$ at that covector with $Au \in H^t_{\mathrm{loc}}(X)$. Since $s \le t$, local Sobolev monotonicity gives $H^t_{\mathrm{loc}}(X) \subset H^s_{\mathrm{loc}}(X)$, so the same cutoff certifies absence from $WF^s(u)$. This proves the contrapositive of $WF^s(u) \subset WF^t(u)$. [/proofplan] [step:Choose a covector outside the higher-order Sobolev wave front set] Let $q \in T^*X \setminus \{0\}$ be a covector such that $q \notin WF^t(u)$. By the defining convention for the Sobolev wave front set, there exists an elliptic microlocal cutoff $A$ at $q$ such that \begin{align*} Au \in H^t_{\mathrm{loc}}(X). \end{align*} Here $A$ is the same microlocal cutoff that appears in the definition of absence from $WF^t(u)$. [/step] [step:Lower the Sobolev order of the microlocalized distribution] Since $s \le t$, local Sobolev monotonicity gives \begin{align*} H^t_{\mathrm{loc}}(X) \subset H^s_{\mathrm{loc}}(X). \end{align*} Applying this inclusion to the distribution $Au$ gives \begin{align*} Au \in H^s_{\mathrm{loc}}(X). \end{align*} Thus the same elliptic microlocal cutoff $A$ at $q$ satisfies the regularity condition required for absence from $WF^s(u)$. [guided] The only analytic input is the monotonicity of local Sobolev spaces: higher Sobolev regularity implies lower Sobolev regularity. Concretely, because $s \le t$, the standard local Sobolev inclusion says \begin{align*} H^t_{\mathrm{loc}}(X) \subset H^s_{\mathrm{loc}}(X). \end{align*} This is the local version of the usual Sobolev scale monotonicity, applied in coordinate charts and then localized by compactly supported cutoffs. We apply this statement to the specific distribution $Au$. From the previous step, the definition of $q \notin WF^t(u)$ gave \begin{align*} Au \in H^t_{\mathrm{loc}}(X). \end{align*} Since every element of $H^t_{\mathrm{loc}}(X)$ is also an element of $H^s_{\mathrm{loc}}(X)$ when $s \le t$, it follows that \begin{align*} Au \in H^s_{\mathrm{loc}}(X). \end{align*} The important point is that no new microlocal cutoff is needed. The operator $A$ was already elliptic at $q$, and ellipticity is independent of the Sobolev order being tested. Therefore the same $A$ now certifies that $q$ is also absent from $WF^s(u)$. [/guided] [/step] [step:Translate the cutoff certificate back into wave front set membership] By the defining convention for $WF^s(u)$, the existence of an elliptic microlocal cutoff $A$ at $q$ with \begin{align*} Au \in H^s_{\mathrm{loc}}(X) \end{align*} implies \begin{align*} q \notin WF^s(u). \end{align*} We have proved that every $q \in T^*X \setminus \{0\}$ satisfying $q \notin WF^t(u)$ also satisfies $q \notin WF^s(u)$. Equivalently, \begin{align*} T^*X \setminus \{0\} \setminus WF^t(u) \subset T^*X \setminus \{0\} \setminus WF^s(u). \end{align*} Taking contrapositives gives \begin{align*} WF^s(u) \subset WF^t(u). \end{align*} This is the desired monotonicity in Sobolev order. [/step]