Comment by Icy0
You can solve this by working backwards from the outside in, replacing a (b x) with c a b x wherever you can (not inside out, or else you get into an infinite loop!)
A cute alternative expression to solve the curried composition puzzle is c c c c c, just 5 c's in a row :)
Finally, Lean is a great language to do these puzzles in. See the following code:
/-- Compose! -/
def c (g : β → γ) (f : α → β) := g ∘ f
/-
?f (?g (?h ?x))
-/
#reduce c (c c) c ?f ?g ?h ?x
/-
?f (?g (?h ?x))
-/
#reduce c c c c c ?f ?g ?h ?x
I used Lean too earlier today :-)
I saw what each #reduce c c ... c did to explore the "palette" I had to work with, and then accidentally stumbled upon the answer that way. I also stumbled on the c (c c) c solution.
May as well include a formalized proof while we're at it: