[Merged by Bors] - chore(Data.NNRat.Defs): reduce imports

[mattrobball]

A more straightforward proof and we can reduce the explicit imports for Data.NNRat.Defs by a third.

---

[github-actions]

PR summary db3fccb641

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.NNRat.Defs	458	444	-14 (-3.06%)
Mathlib.Data.Nat.Hyperoperation	504	490	-14 (-2.78%)
Mathlib.Data.Int.Star	523	510	-13 (-2.49%)
Mathlib.Data.Rat.Star	540	529	-11 (-2.04%)
Mathlib.NumberTheory.EllipticDivisibilitySequence	535	527	-8 (-1.50%)
Mathlib.Data.Nat.Fib.Basic	617	608	-9 (-1.46%)
Mathlib.Data.Nat.Nth	658	650	-8 (-1.22%)
Mathlib.Data.Num.Prime	547	542	-5 (-0.91%)
Mathlib.Data.Nat.Digits	658	653	-5 (-0.76%)

Import changes for all files

Files	Import difference
Too many changes (364)!

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[grunweg]

Looks great; thanks! Feel free to maintainer merge on my behalf. The CI failure looks intermittent; I've just retried it. (Edit: now CI actually runs)

[grunweg]

CI passes, the changes still look good to me - thank you for doing this!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style