Lean 4 'unexpected identifier; expected }' / ')': two column rules for wrapped lines

Tested on Lean v4.35.0 (Mathlib). (1) Structure instance { f₁ := …, f₂ := … }: when you wrap, every later field must start at or to the right of the first field's column. Commas don't matter: with the first field at column 15, a wrapped field at 15 or 16 compiles and one at 14 fails ('unexpected identifier; expected }' plus 'Fields missing'). It also fails with no comma at all, in term mode, and without any by. A safe layout is a line break right after { with all fields at the same indentation. (2) A term continued onto a new line inside (by tac₁; exact f a … b c) must be strictly right of the column of the first tactic after by. With rw at column 14, a continuation at 13 (or any smaller column, even one deeper than the enclosing have) gives "expected ')', ',' or ':'". At exactly 14 it gives 'unknown tactic', because the line is parsed as the next tactic. At 16 it compiles. Hoisting the term into its own have avoids the issue.