mathlib

57ac39bd - chore(data/real/ennreal): drop some lemmas (#18501)

chore(data/real/ennreal): drop some lemmas (#18501) Drop lemmas that are in fact more general lemmas applied to `ennreal`. For now, these lemmas are marked as `@[deprecated]` in leanprover-community/mathlib4#2388.