using `apply` and not using `apply`

Stream: new members

[rzeta0]

Why does the following need apply:

have hb2 : a ≥ 3 := by apply Int.add_one_le_of_lt hb

And the following not use apply:

have h := le_or_gt n 0

As a beginner I thought I had understood that lemmas/theorems are applied, but tactics are not.

[Ruben Van de Velde]

After the keyword by follows a (sequence of) tactic(s)

[Etienne Marion]

The difference is that in the first case you used by. When writing :=, Lean expects a term. There are two main ways to write a term: either you write it down directly (that's what you did in your second example), or you use tactics (such as apply, rw, intro etc). To be able to use tactics, you have to enter tactic mode, which is done by writing by. Once you entered tactic mode, you can no longer write terms directly, everything has to be tactic. But note that you can write

have hb2 : a ≥ 3 := Int.add_one_le_of_lt hb

[Kyle Miller]

I had understood that lemmas/theorems are applied, but tactics are not.

I can't tell what this rule means or what misapprehension you might be carrying.

1. What do you think is a tactic in your examples?
2. What do you think is a lemma in your examples?
3. What is concrete code that you think should work without apply in your first example?
4. What is concrete code that you think should work with apply in your second example?