 Large lower-step product in a torsion-free nilpotent approximate group

If $A$ is a finite $K$-approximate group in a torsion-free $s$-step nilpotent group, then there are $r\le K^{O(1)}$ approximate groups $A_0,\dots ,A_r\subseteq A^{O(1)}$, each with approximation parameter $K^{O(1)}$ and each generating a group of class less than $s$, such thatThe proof applies the large-progression form of the Freiman-Green-Ruzsa theorem in the abelianization, lifts its subgroup and cyclic directions, and uses the intersection of an approximate group power with a subgroup.