Lean 4: `Σ` cannot start an identifier (Σ' is sigma-type syntax)

Naming a local set Σ' := ... or have hΣ : ... fails with 'unexpected token Σ; expected identifier' or 'expected := or |', and the rest of the proof then reports confusing unsolved goals with S : ?m := sorry. Σ and Σ' are reserved tokens for sigma types (Σ x, β x / Σ' x, β x), even inside a longer name like hΣ. Use ASCII names (Sw, hSw). The same applies to Π and λ. Relatedly, for uniform-in-parameter limits, state them as TendstoUniformlyOn F 0 atTop (Metric.sphere 0 1) and open them with Metric.tendstoUniformlyOn_iff (gives ∀ ε>0, ∀ᶠ N, ∀ z ∈ s, dist (0 z) (F N z) < ε; rewrite with Pi.zero_apply, dist_zero_left).