Trouble with example in MIL Section 2.4

Stream: new members

[JK]

I'm mystified why the following proof does not work, since the first calc block seems fine and the second one is symmetric. What am I doing wrong?

import Mathlib
variable (a b c d : ℝ)

theorem aux : min a b + c ≤ min (a + c) (b + c) := by
  apply le_min
  calc
    min a b + c ≤ a + c := by rel [min_le_left a b]
  calc
    min a b + c ≤ b + c := by rel [min_le_right a b]

[Aaron Liu]

it's because one-line calc block are not supported since they cause parse errors

[James Sundstrom]

Also, one-line calc blocks are not necessary because you can do them without calc:

import Mathlib
variable (a b c d : ℝ)

theorem aux : min a b + c ≤ min (a + c) (b + c) := by
  apply le_min
  · rel [min_le_left a b]
  · rel [min_le_right a b]

[JK]

Hmm...then why does the first one-line calc block work?

[Ruben Van de Velde]

It doesn't. If you replace the second calc by sorry, you still get an error

[Kenny Lau]

one line calc block is basically equivalent to change

[Aaron Liu]

it's trying to interpret the second calc statement as a calc line

[JK]

OK, I found it strange since the one-line calc block in

import Mathlib
variable (a b c d : ℝ)

theorem aux' : min a b + c ≤ a + c := by
  calc
    min a b + c ≤ a + c := by rel [min_le_left a b]

does work.

[Aaron Liu]

that's because it's the last tactic in the sequence