When is the lean 4 "by" required?

I am reading an introductory math/lean course here, and got confused about when the tactic/keyword by is required. It is used most of the time, but is occasionally omitted.

For example, it works both with and without by here:

example : 1 + 1 = 2 := sorry
example : 1 + 1 = 2 := by sorry


But for other tactics, it only works with the by:

example : 1 + 1 = 2 := by ring


without the by, it didn't work:

example : 1 + 1 = 2 := ring


The hover hint says:

by tac constructs a term of the expected type by running the tactic(s) tac.

But it is not informational enough for me to understand why it is required some times while not in other occasions.

When is the by required?

I am more interested in this from the perspective of a math learner (who does not know much about programming), not a computer scientist's view about terms and types. In doing a proof, when should one say "by some tactic" versus just "some tactic".

• sorry, calc and rfl are the three I recall in both modes. I think each has a different reason they exist in both. For example rfl is just a theorem, and it is instead Lean’s unifier which makes it so powerful to the point that it looks like a tactic. (Also I recall there are subtle differences between rfl and by rfl.). I think calc is a macro, and I don’t know about sorry. But in general don’t expect you can get by without by unless you are writing a pure term proof and only using a select few built-in macros like the above ones and the sideways triangle symbol ▸ (\t). Commented Jun 5 at 0:27
• This topic is also discussed here on the Lean Zulip: leanprover.zulipchat.com/#narrow/stream/113489-new-members/… Commented Jun 21 at 13:20

To complement the other answer, by is used to start tactic mode proofs (from inside term mode). The most common setting for this is in a top-level theorem such as:

theorem n_plus_m_eq_m_plus_n (n m : Nat) : n + m = m + n := by
-- now in tactic mode
simp  -- apply tactic simp


However, there are a number of more subtle situations where := is also used to start a proof and by is needed to write tactics. Without the by, then one would be giving a term proof instead of a tactic proof.

example : True := by
-- tactic mode
have h0 : True ∨ False -> True := by
-- this is a tactic proof inside a tactic proof
intro h
trivial
-- back to outer tactic block
have h1 : True ∨ False :=
-- this is a term proof (inside a tactic proof)
Or.inl True.intro
-- back to outer tactic block
apply h0
exact h1

example : 1 + 2 = (1 * 1)  + (1 + 1) := by
-- in tactic mode, but we didn't have to be since calc also works in term mode
calc
1 + 2 = 1 + (1 + 1) := by
-- in tactic mode inside calc block inside tactic mode
rfl  -- rfl the tactic
_     = (1 * 1) + (1 + 1) :=
-- in term mode inside calc block inside tactic mode
rfl  -- rfl the term


An advanced application is where one goes into tactic mode in the middle of a term proof. It is rare, but one case is where one starts with a match or recursion like the following:

theorem foo : (n : Nat) -> (n = 0 ∨ n > 0)
| 0 => by
-- tactic mode inside recursion
simp
| n+1 =>
-- term mode inside recursion
Or.inr (Nat.zero_lt_succ n)


But here are some more cases where I've seen this sort of thing:

example : ∀ (n : Nat),  n + 1 = 1 + n :=
-- term proof
fun n => by
-- entering tactic mode in the middle of a term proof


This is sort of a dumb example. It would be better to do the whole thing in tactic mode with intro n at the start.

Sometimes by is nice for making an inline lemma on the spot.

example : ∀ (n : Nat), n + 0 = 0 + n := by
-- tactic mode
intro n
-- normally put
-- here I'm applying rw with the term (Nat.add_zero n)
-- here I'm applying rw with the term (by simp : (∀ n : Nat, 0 + n = n))
-- this is going into tactic mode and using simp to prove the goal ∀ n : Nat, 0 + n = n
rw [(by simp : (∀ n : Nat, 0 + n = n))]


Finally, as for the foo example above, here is one way to write it in tactic mode. Note we don't use by to give the subproofs. We are still in tactic mode.

theorem foo' (n : Nat) : (n = 0 ∨ n > 0) := by
-- tactic mode
induction n with
| zero =>
-- no by required here.  Still in tactic mode.
simp
| succ n ih =>
-- no by required here.  Still in tactic mode.
simp


How to know if you are in tactic mode or term mode?

If you see a goal in the info view, you are likely in tactic mode. If you don't but do see a goal if you write _, then you are in term mode.

You can also write tactics like done. If it says "unknown identifier done" then you are in term mode. Otherwise, if it tells you you have unsolved goals, you are in tactic mode.

by is always required to use tactics. However, there exists some syntactic constructions that have the same name as tactics. sorry is a good example: it is both a syntactically valid tactic and a valid expression. They serve the same purpose, and Lean is setup this way so that you can always use sorry no matter the context, but they should not be confused. When you use sorry as an expression, it's, well, an expression, just like true or 3 + 4. When you use it as a tactic, it's a piece of program whose purpose is to generate a piece of a proof.

From a mathematician perspective, you should always use by unless you have a good reason not to.

To expand on Jason Rute's comment,

• The rfl expression is like Eq.refl a (which is a proof of a = a), except that the a is implicitly figured out by Lean. The rfl tactic (that is, the one you have when you do by rfl), on the other hand, is a bit more general. It tries to match the current goal with things that "look like" that should be closed by "reflexivity", which includes goals like a = a, but also P ↔ P.
• The sorry expression is a macro that essentially just produces a proof (or any value, really) for anything, based on a postulated axiom sorryAx. It's a macro, and not just a plain value, because it also setup things so that error reporting is a little bit better, but you can really think of it just as a value with any type. The sorry tactic, on the other hand, is simply a shorthand for exact sorry. So when you do by sorry, it's really the same thing as just sorry.
• as for calc, I'm not exactly sure why there would be an expression version, but, as far as I understand it, it's pretty much equivalent to its tactic counterpart.
• Can i use by at the end of the first line of a proof which essentially sets out the theorem to be proven (name, variable types, hypotheses, overall goal)? I've seen some proofs that have := by then calc on the next line, and some that don't := and have calc on the next line. Commented Jun 20 at 21:47
• @Penelope As this answer says calc is one of the few identifiers which works both as a tactic and as a term, so you can use it in either circumstance. Basically whenever you have := starting a proof then if you want to use tactics (which you probably want to do until you know more lean) use by. Commented Jun 20 at 23:44