mathlib

e07a24a1 - 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.