From what I've seen on Tao's YouTube channel, he does use GitHub Copilot via VSCode to write Lean4 code.