Comment by IshKebab

Lean does symbols very well. You can just type \r and it will replace it with a right arrow as you type.