good habit to use `:= by` at end of first proof header line?

Stream: new members

[rzeta0]

My apologies if I've asked this previously.

Question - is it a good habit to add by to the end of the first proof header line?

Example 1 without:

-- 01 - First Proof

import Mathlib.Tactic

example {a : ℕ} (h1: a = 4) : a > 1 :=
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

Example 2 with

-- 01 - First Proof

import Mathlib.Tactic

example {a : ℕ} (h1: a = 4) : a > 1 := by -- < with `by`
  calc
    a = 4 := by rw [h1]
    _ > 1 := by norm_num

I think I have learned that with calc it is not strictly necessary.

Is there any harm is promoting := by to beginners like myself?

[Julian Berman]

For beginners it's fine I think.

[Chris Bailey]

by puts you in tactic mode, so it sort of depends on whether you want to be in tactic mode. Being in tactic mode just means that the stuff after by will be parsed and elaborated differently than it would be sans out. I guess calc has both a term and a tactic parser so you don't strictly need the by.

[Ruben Van de Velde]

Yeah, I think we should not confuse beginners by talking about tactic mode and just use by consistently in materials for them

[rzeta0]

Ruben Van de Velde said:

Yeah, I think we should not confuse beginners by talking about tactic mode and just use by consistently in materials for them

Amen to that :)

I will update my beginner tutorials to include by.

I ran into the issue today as I develop the next example code which uses obtain not calc for the first time.