Broken chain of calcs

Stream: new members

[Darij Grinberg]

This is me trying to prove something about points (triples of reals) as defined at the end of MiL section 7.1.

example : (⟨1, 2, 3⟩ : Point) + (⟨2, 5, 9⟩ : Point) = (⟨3, 7, 12⟩ : Point) := by
  ext
  calc ({ x := 1, y := 2, z := 3 } + { x := 2, y := 5, z := 9 }).x
  _ = 1 + 2 := rfl
  _ = 3 := by norm_num
  calc ({ x := 1, y := 2, z := 3 } + { x := 2, y := 5, z := 9 }).y
  _ = 2 + 5 := rfl
  _ = 7 := by norm_num
  calc ({ x := 1, y := 2, z := 3 } + { x := 2, y := 5, z := 9 }).z
  _ = 3 + 9 := rfl
  _ = 12 := by norm_num

The ext creates three goals. For some reason, the first calc correctly closes the first one, but the second (while registering as correct!) fails to close the second one, and the third is misunderstood as trying to solve the second goal. What's going wrong? I had similar issues in another proof. I can fix them by turning the calcs into haves, but I'd like to undersrtand what is goign wrong here.

[Darij Grinberg]

Interestingly, the problem goes away once I structure the argument using · , but then I have to remind Lean about the proper type for the {...}s (by tyepcasting them as Point).

[Aaron Liu]

At first glance I would guess a parsing problem, the first calc only ends when you unindent the lines but you haven't done the so it's interpreting the second calc as the next line of the first calc

[Darij Grinberg]

Interesting! So calc goes naturally with · then

[Darij Grinberg]

Reasonably so, I guess, given that it's a final tactic

[Darij Grinberg]

thank you!

[Ruben Van de Velde]

Does it help if you add an additional two spaces before each _ =?

[Darij Grinberg]

That works, too!

[Kevin Buzzard]

If the ext creates three goals then really your next move should be to add three \cdots to get back to one goal, three times.