chore(Algebra/Order/Ring/Unbundled/Rat): golf

Author: SnirBroshi

Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

@@ -28,19 +28,14 @@ namespace Rat
 
 variable {a b c p q : ℚ}
 
-@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b := by
-  simpa using divInt_nonneg ha (Int.natCast_nonneg _)
+@[simp] lemma mkRat_nonneg {a : ℤ} (ha : 0 ≤ a) (b : ℕ) : 0 ≤ mkRat a b :=
+  divInt_nonneg ha <| Int.natCast_nonneg _
 
-theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) :
-    0 ≤ Rat.ofScientific m s e := by
+theorem ofScientific_nonneg (m : ℕ) (s : Bool) (e : ℕ) : 0 ≤ Rat.ofScientific m s e := by
   rw [Rat.ofScientific]
   cases s
-  · rw [if_neg (by decide)]
-    refine num_nonneg.mp ?_
-    rw [num_natCast]
-    exact Int.natCast_nonneg _
-  · rw [if_pos rfl, normalize_eq_mkRat]
-    exact Rat.mkRat_nonneg (Int.natCast_nonneg _) _
+  · exact num_nonneg.mp <| Int.natCast_nonneg _
+  · grind [normalize_eq_mkRat, Rat.mkRat_nonneg]
 
 instance _root_.NNRatCast.toOfScientific {K} [NNRatCast K] : OfScientific K where
   ofScientific (m : ℕ) (b : Bool) (d : ℕ) :=
@@ -58,7 +53,7 @@ protected lemma divInt_le_divInt {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
   simp [sub_eq_add_neg, ne_of_gt b0, ne_of_gt d0, Int.mul_pos d0 b0]
 
 protected lemma lt_iff_le_not_ge (a b : ℚ) : a < b ↔ a ≤ b ∧ ¬b ≤ a := by
-  rw [← Rat.not_le, and_iff_right_of_imp Rat.le_total.resolve_left]
+  grind
 
 instance linearOrder : LinearOrder ℚ where
   le_refl _ := Rat.le_refl
@@ -74,21 +69,21 @@ theorem mkRat_nonneg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : 0 ≤ mkRat a b 
   divInt_nonneg_iff_of_pos_right (show 0 < (b : ℤ) by simpa using Nat.pos_of_ne_zero hb)
 
 theorem mkRat_pos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : 0 < mkRat a b ↔ 0 < a := by
-  grind [lt_iff_le_and_ne, mkRat_nonneg_iff, Rat.mkRat_eq_zero]
+  grind [mkRat_nonneg_iff, Rat.mkRat_eq_zero]
 
 theorem mkRat_pos {a : ℤ} (ha : 0 < a) {b : ℕ} (hb : b ≠ 0) : 0 < mkRat a b :=
   (mkRat_pos_iff a hb).mpr ha
 
 theorem mkRat_nonpos_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : mkRat a b ≤ 0 ↔ a ≤ 0 := by
-  grind [lt_iff_not_ge, mkRat_pos_iff]
+  grind [mkRat_pos_iff]
 
 theorem mkRat_nonpos {a : ℤ} (ha : a ≤ 0) (b : ℕ) : mkRat a b ≤ 0 := by
   obtain rfl | hb := eq_or_ne b 0
   · simp
   · exact (mkRat_nonpos_iff a hb).mpr ha
 
 theorem mkRat_neg_iff (a : ℤ) {b : ℕ} (hb : b ≠ 0) : mkRat a b < 0 ↔ a < 0 := by
-  grind [lt_iff_not_ge, mkRat_nonneg_iff]
+  grind [mkRat_nonneg_iff]
 
 theorem mkRat_neg {a : ℤ} (ha : a < 0) {b : ℕ} (hb : b ≠ 0) : mkRat a b < 0 :=
   (mkRat_neg_iff a hb).mpr ha
@@ -125,21 +120,11 @@ instance : AddLeftMono ℚ where
 theorem div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) :
     (a : ℚ) / b < c / d ↔ a * d < c * b := by
   simp only [lt_iff_le_not_ge]
-  apply and_congr
-  · simp [div_def', Rat.divInt_le_divInt b_pos d_pos]
-  · simp [div_def', Rat.divInt_le_divInt d_pos b_pos]
+  simp [*, div_def', Rat.divInt_le_divInt]
 
 theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den := by simp [Rat.lt_iff]
 
 theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by
-  rcases le_total q 0 with hq | hq
-  · rw [abs_of_nonpos hq]
-    rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt (mod_cast q.pos) Int.zero_lt_one,
-      mul_one, zero_mul] at hq
-    rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def]
-  · rw [abs_of_nonneg hq]
-    rw [← num_divInt_den q, ← zero_divInt, Rat.divInt_le_divInt Int.zero_lt_one (mod_cast q.pos),
-      mul_one, zero_mul] at hq
-    rw [Int.natAbs_of_nonneg hq, num_divInt_den]
+  grind [abs_of_nonpos, neg_def, Rat.num_nonneg, abs_of_nonneg, num_divInt_den]
 
 end Rat