expected command, expected :=, expected structure

Stream: mathlib4

[Heather Macbeth]

There have been several reports of people getting bugs like expected command or expected structure:
1 2 3 4 5

I now have one of my own, on the following code:

import Mathlib.Init.ZeroOne

variable {α : Type _} [Mul α] [Zero α]

lemma eq_zero_or_eq_zero_of_mul_eq_zero {a b : α} (h : a * b = 0) : a = 0 ∨ b = 0 := sorry

It seems to be a feature of this bug that it is not reproducible, so I don't know if it's even worth reporting, but thought I would try!

[Heather Macbeth]

Locally, for me, it persisted through some mwe-ification, descending from expected := to expected | to expected command. And I have the impression that initially it was connected to poor focusing (e.g. having multiple goals around in a way that good · would prevent), but haven't confirmed this yet (and now I need to go to bed!).

[Mario Carneiro]

I can replicate this. I think the issue is that Mathlib.Init.ZeroOne doesn't import the lemma command

[Mario Carneiro]

that doesn't explain the other error messages so you might have MWE'd too far

[Heather Macbeth]

Oops! ... I'll try again tomorrow.

[Reid Barton]

I got an expected } once too, at top level, between variable statements

[Reid Barton]

that was baffling

[Heather Macbeth]

OK, second try. Not minimized yet but I'll return to this in an hour if someone doesn't fix it first.

import Mathlib.Data.Rat.Cast

variable [MonoidWithZero α] [NoZeroDivisors α]

example {a : α} (ha : a ^ 2 = 0) : a = 0 := by
  have : a = 0 ∨ a = 0
  apply eq_zero_or_eq_zero_of_mul_eq_zero
  calc a * a = a ^ 2 := sorry
  _ = 0 := sorry
  obtain ha | ha := this -- expected ':='

[Reid Barton]

I think the next to last line should be indented, if the tactic block is to continue after calc

[Heather Macbeth]

Ah, nice! That's an easy rule to remember.

[Reid Barton]

I am not actually sure how Lean interprets what you wrote above, but it must think the calc block is either 1 or 3 lines, and not exactly 2.