limitations of functions on struct defined w pattern match

Stream: new members

[Nicolas Rolland]

"Math in lean" 6.1 states about functions on structures defined using pattern matching :

Although it is sometimes convenient to define functions this way, the definitional properties are not as convenient. For example, the expressions addAlt a b and addAlt' a b cannot be simplified until we decompose a and b into components, which we can do with cases, rcases, etc.

But when I comment out the mentioned bits, it stills typecheck (including with simp only)
Is it still relevant or has it been invalidated with lean 4 ?

@[ext]
structure Point where
  x : ℝ
  y : ℝ
  z : ℝ

def addAlt : Point → Point → Point
  | Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => ⟨x₁ + x₂, y₁ + y₂, z₁ + z₂⟩

example (a b : Point) : addAlt a b = addAlt b a := by
  --rcases a with ⟨xa, ya, za⟩
  --rcases b with ⟨xb, yb, zb⟩
  simp [addAlt, add_comm]

[Eric Wieser]

This changed in lean 4, though I think I opened an issue asking it to be changed back!