refactor(data/real/irrational): review (#2304)
refactor(data/real/irrational): review (#2304)

* refactor(data/real/irrational): review

* Update src/data/real/irrational.lean

* Update src/data/real/irrational.lean

* Apply suggestions from code review

Co-authored-by: sgouezel <06bcd766296da4e7f3f1690c64fbdb3ee30e2f66@univ-rennes1.fr>
Co-authored-by: Scott Morrison <625600233cb3bcab32268c17610882e0fdaed295@tqft.net>
Co-authored-by: mergify[bot] <b09a6ee808b67e98a221404e7aaa52e0398a4954@users.noreply.github.com>
leanprover-community/mathlib,leanprover-community/mathlib