The omega tactic

Stream: general

[Donald Sebastian Leung]

The omega tactic is currently documented in the Lean mathlib documentation but this simple example fails with unknown identifier 'omega':

example : 1 + 1 = 2 :=
begin
  omega
end

How do I import the omega tactic?

[Alex J. Best]

import tactic.omega

[Donald Sebastian Leung]

Thanks, that worked

[Floris van Doorn]

In general, if you write import tactic you get all tactics in mathlib.