Commit 2026-10-17 17:39 bac53ecd

feat(Linter/Style): lint against ∀ᵉ/∃ᵉ (#44544) The ∀ᵉ/∃ᵉ notation is used rarely in mathlib, so to many users it is an unfamiliar notation. Therefore, it would be better to simply not use it. This PR adds a linter against the notation, which comes with a Try this suggestions that replaces the notation with uses of plain ∀/∃

• The adaptations have been generated fully automatically using these Try this suggestions. So, it is easiest to review this PR commit by commit.
• The ∃ᵉ notation is still used in one place, namely in the macro that defines the {_ | _} notation for sets. The linter explicitly does not flag this.
• This linter would fit in very nicely into the framework of #44496. That can be done in a follow-up PR after that is merged, and will remove the slowdown that this PR adds. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.E2.88.80.E1.B5.89.2F.E2.88.83.E1.B5.89.20notation/with/629610458