chore(data/real/hyperreal): remove @ in a proof (#8063)
chore(data/real/hyperreal): remove @ in a proof (#8063)

Remove @ in a proof.  Besides its clear aesthetic value, this prevents having to touch this file when the number typeclass arguments in the intervening lemmas changes.

See PR #7645 and #8060.






leanprover-community/mathlib,leanprover-community/mathlib