I would like know if there's anything wrong with the following proof.
Claim. Let $f : X \rightarrow S$ be a finite etale of degree $n$. Then there is a noncanonical isomorphism $f^*X \cong \amalg_n X$.
Proof by induction on $n$. For $n = 1$, a finite etale morphism of degree 1 must be an isomorphism $S \rightarrow S$, so we are done. For the induction step, assume the claim for all etale morphisms of degree $n-1 \ge 1$ and let $f : X \rightarrow S$ be finite etale of degree $n$. The diagonal $X \rightarrow f^* X$ is a clopen immersion that splits off a component isomorphic to $X$, hence $f^* X \cong X \amalg X'$ where $X' \rightarrow X$ is a finite etale morphism of degree $n-1$. By induction hypothesis we are done.
The above proof is a slight alteration of the proof of Stacks Project Lemma 40.18.3, which claims that there IS a trivializing etale cover for $X$. I was surprised that I couldn't find a single source that remarks that we can just take the trivializing cover to be $X$ itself. Is there something wrong with my claim?