Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.

I mostly write lean4 now and emit proof-carrying System F Omega via rfl. It's the right level of abstraction when the droids have been pinned to theory laden symbolisms. It's also just pleasant to use.