chore(Data.NNRat.Defs): reduce imports (#14541)

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

Author: mattrobball

Mathlib/Data/Int/Star.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Star.Order
 import Mathlib.Algebra.Order.Monoid.Submonoid
+import Mathlib.Algebra.Order.Ring.Basic
 
 /-!
 # Star ordered ring structure on `ℤ`

Mathlib/Data/NNRat/Defs.lean

@@ -5,7 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Order.Nonneg.Ring
 import Mathlib.Algebra.Order.Ring.Rat
-import Mathlib.Data.Int.Lemmas
 
 #align_import data.rat.nnrat from "leanprover-community/mathlib"@"b3f4f007a962e3787aa0f3b5c7942a1317f7d88e"
 
@@ -32,7 +31,6 @@ Whenever you state a lemma about the coercion `ℚ≥0 → ℚ`, check that Lean
 `Subtype.val`. Else your lemma will never apply.
 -/
 
-
 open Function
 
 deriving instance CanonicallyOrderedCommSemiring for NNRat
@@ -376,11 +374,8 @@ lemma coprime_num_den (q : ℚ≥0) : q.num.Coprime q.den := by simpa [num, den]
 @[simp] lemma den_ofNat (n : ℕ) [n.AtLeastTwo] : den (no_index (OfNat.ofNat n)) = 1 := rfl
 
 theorem ext_num_den (hn : p.num = q.num) (hd : p.den = q.den) : p = q := by
-  refine ext <| Rat.ext ?_ ?_
-  · apply (Int.natAbs_inj_of_nonneg_of_nonneg _ _).1 hn
-    · exact Rat.num_nonneg.2 p.2
-    · exact Rat.num_nonneg.2 q.2
-  · exact hd
+  refine ext <| Rat.ext ?_ hd
+  simpa [num_coe]
 #align nnrat.ext_num_denom NNRat.ext_num_den
 
 theorem ext_num_den_iff : p = q ↔ p.num = q.num ∧ p.den = q.den :=

Mathlib/Data/Nat/Digits.lean

@@ -628,7 +628,7 @@ theorem digits_two_eq_bits (n : ℕ) : digits 2 n = n.bits.map fun b => cond b 1
   cases b
   · rw [digits_def' one_lt_two]
     · simpa [Nat.bit, Nat.bit0_val n]
-    · simpa [pos_iff_ne_zero, Nat.bit0_eq_zero]
+    · simpa [Nat.bit, pos_iff_ne_zero, Nat.bit0_eq_zero]
   · simpa [Nat.bit, Nat.bit1_val n, add_comm, digits_add 2 one_lt_two 1 n, Nat.add_mul_div_left]
 #align nat.digits_two_eq_bits Nat.digits_two_eq_bits
 

Mathlib/Data/Nat/Fib/Basic.lean

@@ -6,6 +6,7 @@ Authors: Kevin Kappelmann, Kyle Miller, Mario Carneiro
 import Mathlib.Algebra.BigOperators.Group.Finset
 import Mathlib.Data.Finset.NatAntidiagonal
 import Mathlib.Data.Nat.GCD.Basic
+import Mathlib.Data.Nat.Bits
 import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Logic.Function.Iterate
 import Mathlib.Tactic.Ring

Mathlib/Data/Nat/Hyperoperation.lean

@@ -3,7 +3,6 @@ Copyright (c) 2023 Mark Andrew Gerads. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mark Andrew Gerads, Junyan Xu, Eric Wieser
 -/
-import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Tactic.Ring
 
 #align_import data.nat.hyperoperation from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"

Mathlib/Data/Nat/Nth.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Vladimir Goryachev. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Vladimir Goryachev, Kyle Miller, Scott Morrison, Eric Rodriguez
 -/
+import Mathlib.Data.List.GetD
 import Mathlib.Data.Nat.Count
 import Mathlib.Data.Nat.SuccPred
 import Mathlib.Order.Interval.Set.Monotone

Mathlib/Data/Num/Prime.lean

@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import Mathlib.Data.Num.Lemmas
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Tactic.Ring
+import Mathlib.Algebra.Ring.Divisibility.Basic
 
 #align_import data.num.prime from "leanprover-community/mathlib"@"58581d0fe523063f5651df0619be2bf65012a94a"
 

Mathlib/Data/Rat/Star.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux, Yaël Dillies
 -/
 import Mathlib.Algebra.GroupWithZero.Commute
+import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Algebra.Star.Order
 import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Algebra.Order.Monoid.Submonoid

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 David Kurniadi Angdinata. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Kurniadi Angdinata
 -/
-import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Data.Nat.EvenOddRec
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.LinearCombination

scripts/noshake.json

@@ -214,6 +214,7 @@
   "Mathlib.Tactic.Positivity.Basic":
   ["Mathlib.Algebra.GroupPower.Order",
    "Mathlib.Algebra.Order.Group.PosPart",
+   "Mathlib.Algebra.Order.Ring.Basic",
    "Mathlib.Data.Int.CharZero",
    "Mathlib.Data.Nat.Factorial.Basic",
    "Mathlib.Data.PNat.Defs"],