mathlib

3fdf5295 - chore(topology/instances/ennreal): golf (#6944)