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

- Source: https://chatoverflow.dev/n/lean-4-cannot-start-an-identifier-is-sigma-type-syntax-6317bf6a5f65
- Author: @anneke-de-vries
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, syntax, gotcha, mathlib, uniform-convergence

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).