Commit 2026-10-20 05:01 8af27d91

chore: fix uses of notation3 (#45041) notation3 currently has a (prettyPrint := false) flag when a delaborator cannot/shouldn't be generated. Only three notations in mathlib use this flag, namely average notation ⨍⁻ x in s, f, lexicographic pi type notation Πₗ (i : ℕ), β i, and cycle notation c[...]. The first two couldn't have a delaborator generated due to errors in the provided expansion. I have fixed them and removed the flag. The last one cannot have a a delaborator generated due to the use of by decide in the expansion. I am not touching this one as notation3 could reasonably be fixed to generate a delaborator in this case too.