Mechanics of Proof "Or" and proof by cases

Stream: lean4

[Luka Ivanić]

This is a tip for people doing the exercises.
I have been struggling with the syntax while doing an example exercise 2.3.4.

example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
  have h1 :=
    calc
    (x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
    _ = 0 := by rw [hx]
  have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
  obtain h3 | h4 := h2
  left
  calc
    x = 1 := by addarith [h3]
    _ = 1 := by ring

  right
  calc
    x = 2 := by addarith [h4]

This is the correct answer, or at least one way of writing it, however, this has an addition in the "left" block:

    _ = 1 := by ring

Without it, the lean infoview persistently flashes a (syntax) error. So I guess for some reason the calculation block has to have multiple lines.

Of course if anyone can offer an explaination for the syntax behaviour that would be a bonus!

Also, for readability sake, it is also possible to divide the left/right blocks like this:

-- first part of the exercise
  . left
    calc
      x = 1 := by addarith [h3]
      _ = 1 := by ring

  . right
    calc
      x = 2 := by addarith [h4]

[Patrick Massot]

calc is definitely not intended for single line computation. Why don’t you simply write

-- first part of the exercise
  . left
    addarith [h3]
  . right
    addarith [h4]

[Luka Ivanić]

That's amazing! With this improvement, my code is half as long, thank you very much