Gowers' $Fin_k$ theorem is a combinational result about for colorings of a particular family of (countable) partial semigroups with homomorphisms between them where the homogeneity requirement applies to sets generated by both the semigroup operations and the homomorphisms. It has important applications in analysis. The proof uses ultrafilters and indeed spaces of ultrafilters and Zorn's lemma type arguments on various subspaces to produce an ultrafilter that guides the construction of the homogeneous set. We prove that Gowers' theorem is provable in recursive mathematics ($RCA_0$) from a version of a seemingly much simpler special case, Hindman's theorem. Hindman's theorem is known to have a quite elementary proof. So too, then does Gowers'. We will also try to explain what such a proof would be without the metamathematical arguments.