Pretty Symbols in Lean

To produce a pretty symbol in Lean, type the editor shortcut followed by space or tab.

Unicode	Editor Shortcut	Definition
→	\to	function or implies
↔	\iff	if and only if
←	\l	used by the rw tactic
¬	\not	negation operator
∧	\and	and operator
∨	\or	or operator
∃	\exists	there exists quantifier
∀	\forall	for all quantifier
∣	\mid	divisibility [1]
ℕ	\nat	type of natural numbers
ℤ	\int	type of integers
∘	\circ	composition of functions
≠	\ne	not equal to
⟨⟩	\langle and \rangle	used to build complicated types out of simple types

Footnotes

[1]

Be very careful! The symbol for divisibility is not the | symbol on your keyboard. Lean will through a cryptic error if you use it.