fix: make Rat definitions irreducible

see <https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slow.20.60positivity.60/near/322877369>

Std/Data/Rat/Basic.lean

@@ -132,8 +132,9 @@ instance : LE Rat := ⟨fun a b => b.blt a = false⟩
 instance (a b : Rat) : Decidable (a ≤ b) :=
   inferInstanceAs (Decidable (_ = false))
 
-/-- Multiplication of rational numbers. -/
-protected def mul (a b : Rat) : Rat :=
+/-- Multiplication of rational numbers. (This definition is `@[irreducible]` because you don't
+want to unfold it. Use `Rat.mul_def` instead.) -/
+@[irreducible] protected def mul (a b : Rat) : Rat :=
   let g1 := Nat.gcd a.num.natAbs b.den
   let g2 := Nat.gcd b.num.natAbs a.den
   { num := (a.num.div g1) * (b.num.div g2)
@@ -152,8 +153,11 @@ protected def mul (a b : Rat) : Rat :=
 
 instance : Mul Rat := ⟨Rat.mul⟩
 
-/-- The inverse of a rational number. Note: `inv 0 = 0`. -/
-protected def inv (a : Rat) : Rat :=
+/--
+The inverse of a rational number. Note: `inv 0 = 0`. (This definition is `@[irreducible]`
+because you don't want to unfold it. Use `Rat.inv_def` instead.)
+-/
+@[irreducible] protected def inv (a : Rat) : Rat :=
   if h : a.num < 0 then
     { num := -a.den, den := a.num.natAbs
       den_nz := Nat.ne_of_gt (Int.natAbs_pos.2 (Int.ne_of_lt h))
@@ -196,8 +200,11 @@ theorem add.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
     exact Nat.eq_one_of_dvd_one <| b.reduced.gcd_eq_one ▸ Nat.dvd_gcd this <|
       Nat.dvd_trans (Nat.gcd_dvd_left ..) (be ▸ Nat.dvd_mul_right ..)
 
-/-- Addition of rational numbers. -/
-protected def add (a b : Rat) : Rat :=
+/--
+Addition of rational numbers. (This definition is `@[irreducible]` because you don't want to
+unfold it. Use `Rat.add_def` instead.)
+-/
+@[irreducible] protected def add (a b : Rat) : Rat :=
   let g := a.den.gcd b.den
   if hg : g = 1 then
     have den_nz := Nat.ne_of_gt <| Nat.mul_pos a.den_pos b.den_pos
@@ -228,8 +235,10 @@ theorem sub.aux (a b : Rat) {g ad bd} (hg : g = a.den.gcd b.den)
   simp only [show (-b).num = -b.num from rfl, Int.neg_mul] at this
   exact this
 
-/-- Subtraction of rational numbers. -/
-protected def sub (a b : Rat) : Rat :=
+/-- Subtraction of rational numbers. (This definition is `@[irreducible]` because you don't want to
+unfold it. Use `Rat.sub_def` instead.)
+-/
+@[irreducible] protected def sub (a b : Rat) : Rat :=
   let g := a.den.gcd b.den
   if hg : g = 1 then
     have den_nz := Nat.ne_of_gt <| Nat.mul_pos a.den_pos b.den_pos

Std/Data/Rat/Lemmas.lean

@@ -168,7 +168,7 @@ theorem divInt_num_den (z : d ≠ 0) (h : n /. d = ⟨n', d', z', c⟩) :
 theorem add_def (a b : Rat) :
     a + b = normalize (a.num * b.den + b.num * a.den) (a.den * b.den)
       (Nat.mul_ne_zero a.den_nz b.den_nz) := by
-  show Rat.add .. = _; dsimp only [Rat.add]; split
+  show Rat.add .. = _; delta Rat.add; dsimp only; split
   · exact (normalize_self _).symm
   · have : a.den.gcd b.den ≠ 0 := Nat.gcd_ne_zero_left a.den_nz
     rw [maybeNormalize_eq_normalize _ _
@@ -218,7 +218,7 @@ theorem neg_divInt (n d) : -(n /. d) = -n /. d := by
 theorem sub_def (a b : Rat) :
     a - b = normalize (a.num * b.den - b.num * a.den) (a.den * b.den)
       (Nat.mul_ne_zero a.den_nz b.den_nz) := by
-  show Rat.sub .. = _; dsimp only [Rat.sub]; split
+  show Rat.sub .. = _; delta Rat.sub; dsimp only; split
   · exact (normalize_self _).symm
   · have : a.den.gcd b.den ≠ 0 := Nat.gcd_ne_zero_left a.den_nz
     rw [maybeNormalize_eq_normalize _ _
@@ -243,7 +243,7 @@ theorem divInt_sub_divInt (n₁ n₂ : Int) {d₁ d₂} (z₁ : d₁ ≠ 0) (z
 
 theorem mul_def (a b : Rat) :
     a * b = normalize (a.num * b.num) (a.den * b.den) (Nat.mul_ne_zero a.den_nz b.den_nz) := by
-  show Rat.mul .. = _; dsimp only [Rat.mul]
+  show Rat.mul .. = _; delta Rat.mul; dsimp only
   have H1 : a.num.natAbs.gcd b.den ≠ 0 := Nat.gcd_ne_zero_right b.den_nz
   have H2 : b.num.natAbs.gcd a.den ≠ 0 := Nat.gcd_ne_zero_right a.den_nz
   rw [mk_eq_normalize, ← normalize_mul_right _ (Nat.mul_ne_zero H1 H2)]; congr 1

Std/Tactic/Lint/Simp.lean

@@ -66,7 +66,8 @@ def isSimpEq (a b : Expr) (whnfFirst := true) : MetaM Bool := withReducible do
 /-- Constructs a message from all the simp theorems encoded in the given type. -/
 def checkAllSimpTheoremInfos (ty : Expr) (k : SimpTheoremInfo → MetaM (Option MessageData)) :
     MetaM (Option MessageData) := do
-  let errors := (← withSimpTheoremInfos ty fun i => do (← k i).mapM addMessageContextFull).filterMap id
+  let errors :=
+    (← withSimpTheoremInfos ty fun i => do (← k i).mapM addMessageContextFull).filterMap id
   if errors.isEmpty then
     return none
   return MessageData.joinSep errors.toList Format.line