My experience with copilot in lean is that it's just as useful as in programming. It guesses alright and works well for boilerplate, and structure and syntax, but you need to tune by hand whenever you need to do something significant or clever.