An abelian tower of a finite group admits a cyclic refinement — Proposition I.3.1, Lang's 'Algebra' Recently I've been looking through Lang's Algebra, and I encountered a problem in the proof of Proposition 3.1 in Chapter I Groups.

Proposition 3.1. Let $G$ be a finite group. An abelian tower of $G$ admits a cyclic refinement. Let $G$ be a finite solvable group. Then $G$ admits a cyclic tower, whose last element is $\{e\}$.
Proof. The second assertion is an immediate consequence of the first, and it clearly suffices to prove that if $G$ is finite, abelian, then $G$ admits a cyclic tower. We use induction on the order of $G$. Let $x$ be an element of $G$. We may assume that $x \neq e$. Let $X$ be the cyclic group generated by $x$. Let $G' = G/X$. By induction, we can find a cyclic tower in $G'$, and its inverse image is a cyclic tower in $G$ whose last element is $X$. If we refine this tower by inserting $\{e\}$ at the end, we obtain the desired cyclic tower.

I don't understand why it suffices to prove that if $G$ is finite, abelian, then $G$ admits a cyclic tower. In the statement of the proposition $G$ is not assumed to be an abelian group.
Moroever, even assuming that we do prove that if $G$ is finite, abelian, then $G$ admits a cyclic tower, I don't see how can we use this in proving Proposition 3.1.
Maybe this question is very easy, but currently I can't understand it. Any help would be appreciated.
 A: You are assuming we have an abelian tower for the finite group $\;G\;$ :
$$(**)\;\;\;1=G_m\lhd G_{m-1}\lhd\ldots\lhd G_1\lhd G_0:=G\;,\;\;s.t.\;\;G_i/G_{i+1}\;\;\text{abelian}\;\;\forall\,1=0,1,...,m-1 $$
The above means in particular that $\;G_{m-1}\cong G_{m-1}/G_m\;$ is abelian, so by the part marked in red in the proof, there's a cyclic refinement of it: 
$$1= A_0\lhd A_1\lhd\ldots\lhd A_{m_1}:=G_{m-1}\;,\;\;A_k/A_{k+1}\;\;\text{cyclic}$$
But also $\;G_{m-2}/G_{m-1}\;$ is abelian, so again by the red part we've a cyclic refinement
$$G_{m-1}=:B_0\lhd B_1\lhd\ldots\lhd B_{m_2}:=G_{m-2}\;,\;\;B_i/B_{i+1}\;\;\text{cyclic}$$
Observe now that the subrefinement ("sub" because it is a refinement of part of the original tower)
$$1=G_m:=A_0\lhd A_1\lhd\ldots\lhd A_{m_1}=G_{m_1}=B_0\lhd B_1\lhd\ldots\lhd B_{m_2}=G_{m_2}$$
is cyclic! Well, go on like this inductively up through the whole first, original tower (**) ...
A: This is my attempt to answer the question using the help I received from Tobias Kildetoft and Don Antonio.
Suppose that we have proved the assertion that if $G$ is finite, abelian, then $G$ admits a cyclic tower. And we already have an abelian tower for the finite group $G$
$$
1 = G_m \triangleleft G_{m-1} \triangleleft \dots \triangleleft G_1 \triangleleft G_0 :=G, 
$$
such that $G_i/G_{i+1}$ is abelian for all $i = 0,1,\dots,m-1$.
For every abelian group $G_i/G_{i+1}$, there exists a canonical homomorphism $G_i \to G_i/G_{i+1}$. One of the isomorphism theorems says that this map establishes a bijection between subgroups of $G/X$ and subgroups of $G$ that contain $X$. Moreover, this bijection preserves inclusions, normality and quotients. So $G_i/G_{i+1}$ admits a cyclic tower. Then $G_i$ admits a cyclic tower whose last element is $G_{i+1}$. So, for every group $G_i$ ($i=0,\dots,m-1$) there is a cyclic tower whose last element is $G_{i+1}$. Hence, we can refine an abelian tower to a cyclic tower.
A: This answer is also an attempt at Lamport's method of writing structured proofs.[1], [2]


Proposition 3.1.
Assume: $G$ is a finite group having the abelian tower
$$
G = G_0 \supset G_1 \supset G_2 \supset \dotsb \supset G_m.\tag{$*$}
$$
Prove: $(*)$ has a cyclic refinement.

Proof.

*

*It suffices to assume that $m = 1$.
Proof: If each $G_i \supset G_{i+1}$ has a cyclic refinement, so does $(*)$ by concatenating these cyclic towers.

Let $f \colon G \to G/G_1$ be the canonical map.


*It suffices to assume that $G$ is abelian and $G_1 = \{e\}$.
Proof: Since $G/G_1$ is abelian by hypothesis, $G/G_1 \supset \{ \bar{e} \}$ has a cyclic refinement by assumption. The pullback by $f$ of this cyclic tower is a cyclic refinement of $G \supset G_1$.

Let $P(n)$ be the statement that for a finite abelian group $G$ with $|G| = n$, $G \supset \{e\}$ has a cyclic refinement.


*Case: $n = 1$
Proof: Then $G = \{e\}$, and $\{e\} \supset \{e\}$ is already cyclic, so there is nothing to show.


*Assume that there exists $n \geq 1$ such that $P(m)$ is true for all $m \leq n$. Then, $P(n+1)$ is true.
4.1. Pick $x \in G$ such that $x \neq e$.
Proof: Since $|G| = n + 1$ and $n \geq 1$, there exists such an $x$.
Let $X = \langle x \rangle$, and $p \colon G \to G/X$ be the canonical map.
4.2. $G/X \supset \{ \bar{e} \}$ has a cyclic refinement.
Proof: Since $m = |G/X| < |G| = n + 1$, and $P(m)$ is true by assumption.
4.3. QED
Proof: The pullback by $p$ of the cyclic tower obtained in step 4.2. is a cyclic refinement of $G \supset X$. Since $X$ is cyclic, this is also a cyclic refinement of $G \supset \{e\}$.


*QED
Proof: By the principle of strong mathematical induction: step 3. proves the base case and step 4. proves the induction step.
$\blacksquare$
