mathlib3

47a8d5a6 - refactor(data/{sigma,psigma}/order): Use `lex` synonym and new notation (#11235)

refactor(data/{sigma,psigma}/order): Use `lex` synonym and new notation (#11235) This introduces notations `Σₗ i, α i` and `Σₗ' i, α i` for `lex (Σ i, α i)` and `lex (Σ' i, α i)` and use them instead of the instance switch with locale `lex`.