Every normal subgroup of a finite group is contained in some composition series In this context composition series means the same thing as defined here.
As the title says given a finite group $G$ and $H \unlhd G$ I would like to show there is a composition series containing $H.$
Following is my attempt at it.
The main argument of the claim is showing the following.

Lemma. If $H \unlhd G$ and $G/H$ is not simple then there exist a subgroup $I$ such that $H \unlhd I \unlhd G.$

The proof follows from the 4th isomorphism theorem since if $G/H$ is not simple then there is a normal subgroup $\overline{I} \unlhd G/H$ of the form $\overline{I} = H/I.$
Suppose now that $G/H$ is not simple. Using the above lemma we deduce that there exist a finite chain of groups (since $G$ is finite) such that $$H \unlhd I_1 \unlhd \cdots \unlhd I_k \unlhd G$$ and $G/I_k$ is simple. Now one has to repeat this process for all other pairs $I_{i+1}/I_{i}$ and for $I_1/H$ until the quotients are simple groups. This is all fine since all the subgroups are finite as well.
Now if $H$ is simple we are done otherwise there is a group $J \unlhd H$ and we inductively construct the composition for $H.$
Is the above "proof" correct? If so, is there a way to make it less messy?
 A: Yes your proof is essentially correct. You can make it look less messy as follows. Noticing that the proof that $G$ has a composition series in the first place has the same structure as your proof, you could do a two-in-one-blow induction on the order of $G$ by showing: "$G$ has a composition series, and if $H$ is a nontrivial proper normal subgroup of $G$, then it can be chosen to pass through $H$".
The base cases are $G$ trivial or simple, and the statement is obvious then (the second part is vacuously satisfied). Otherwise there exists a nontrivial proper normal subgroup $H$ of $G$; choose it, or for the second part take the one that is imposed. Now by induction $H$ has a composition series, which we stick below $H$ as part of our final composition series. The quotient $G/H$ also has a composition series, which we "lift" by taking the preimage in $G$ (under the projection modulo $H$) of every subgroup in the series to obtain the part of our composition series between $G$ and $H$, by the isomorphism theorem.
A: Suppose you have $A \triangleleft C$ with $C/A$ not simple. Then there is some nontrivial subgroup $B/A \triangleleft C/A$ (by Lattice Isomorphism Theorem), so you can extend $A \triangleleft C$ to $A \triangleleft B \triangleleft C$. By repeating this step you yield a composition series (it is clearly bounded, and will first terminate when all the composition factors are indeed simple).
Take $1 \triangleleft N \triangleleft G$ and apply above step. This constructs a composition series containing $N$.
A: Your approach has all the elements of a proof, but I wanted to offer suggestions for a "less messy" version.
First of all, as long as you are using that "any finite group has a composition series", you shouldn't need your lemma.
You could go about it this way. Let $H$ be a normal subgroup of $G$. Then $H$ has a composition series $1=H_0<\dots<H_k=H$. The group $G/H$ also has a composition series, which we will enumerate this way:
$$
H/H=H_{k}/H<\dots <H_n/H=G/H
$$
By an isomorphism theorem, the fact that $(H_{j}/H)/(H_{j-1}/H)$ is simple is equivalent to $H_j/H_{j-1}$ being simple.
Putting these two chains together, you have that $H_0<\dots <H_n$ is a composition series for $G$ through $H$.
