For most of my computer science PhD the “trick” was just to get the inductive definition to work, and then how to tweak it for the next paper. Or, get enough structuret we can do an “abstract nonsense” proof[0].

[0]:https://ncatlab.org/nlab/show/category+theory#AbstractNonsen...