how to prove of find simple theorem

Stream: maths

[Truong Nguyen]

Hi everyone, I am a new user, my question is maybe too simple. Please make it lear for me.
Can you tell me how to find in the library or prove the simple theorem like:

theorem ttt1 (n m: ℕ ) : n <= m → n < m ∨ n = m :=
sorry

[Mario Carneiro]

the naming convention would call that lt_or_eq_of_le

[Truong Nguyen]

Thank you, but can you tell me how can find the stuffs like this one?

Is there a “search” command to find a theorem in the library?
I am working in some proof, sometime, it looks me quite a lot of time to find simple theorem to use.
For example, I need this one:

theorem tq (a b: ℕ ): ¬ a ≤ b ↔ b < a :=
sorry

Is there a way that I can find or prove it easily? I think it should be easy.
Thank you,
Truong

[Kenny Lau]

import tactic.find tactic.ring

run_cmd tactic.skip

#find ¬ _ ≤ _ ↔ _ < _
-- not_le: ∀ {α : Type u} [_inst_1 : linear_order α] {a b : α}, ¬a ≤ b ↔ b < a

[Kevin Buzzard]

@Truong Nguyen Mario already explained how to find stuff like this -- learn the naming convention :-) Follow the link!

[Truong Nguyen]

Oh, thank you

[Truong Nguyen]

Dear Kenny Lau,
Can you give some instruction for how to use the "#find" command?

[Kevin Buzzard]

import tactic.find

def x := 0 -- or anything -- for some reason you can't use #find immediately

#find _ + _ ≤ _ + _