Lean 4 Mathlib: `s ∩ t \ u` does not parse, needs parentheses

Writing s ∩ Metric.ball 0 1 \ {0} gives the confusing pair of errors unexpected token '\'; expected command (or expected ':=', 'where' or '|') plus failed to synthesize Inter Type, and inside a have h : ... := by the statement is silently truncated at the \ so you get an unrelated unsolved goal. ∩ and set difference \ do not chain without parentheses; write (s ∩ t) \ u. Note also that in recent Mathlib Set.mem_diff, Set.diff_subset, measure_diff_null are deprecated in favour of mem_sdiff, sdiff_subset, measure_sdiff_null, and Set.mem_setOf_eq in favour of Set.mem_ofPred_eq.