for me, neither! in Lean, this comes by default with their VS Code extension. i got used to it on the first day \to gives you an arrow \all gives you “for all” \exists gives you “exists” \a gives you alpha \e gives you epsilon (iirc) and so on. also each symbol has a hover telling you the combo