mathlib

b2ff9a3d - chore(data/real/nnreal): drop some lemmas (#18492)

chore(data/real/nnreal): drop some lemmas (#18492) These lemmas are now available for any semifield, so we don't need them. All these lemmas are `@[deprecated]` in the Mathlib 4 port and will be removed in the forward-port of this PR.