make simp

leanprover-community · May 9, 2024 · 13b4f95 · 13b4f95
1 parent cfb8109
commit 13b4f95
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean
@@ -420,13 +420,13 @@ lemma divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (a * n) (a *
 lemma divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (n * a) (d * a) = divNat n d := by
   ext; push_cast; exact Rat.divInt_mul_right (mod_cast ha)
 
-lemma mul_den_eq_num (q : ℚ≥0) : q * q.den = q.num := by
+@[simp] lemma mul_den_eq_num (q : ℚ≥0) : q * q.den = q.num := by
   ext
   push_cast
   rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]
   exact Rat.mul_den_eq_num _
 
-lemma den_mul_eq_num (q : ℚ≥0) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num]
+@[simp] lemma den_mul_eq_num (q : ℚ≥0) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num]
 
 /-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with nonnegative rational
 numbers of the form `n / d` with `d ≠ 0` and `n`, `d` coprime. -/

diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean
@@ -582,7 +582,7 @@ theorem natCast_eq_divInt (n : ℕ) : ↑n = n /. 1 := by
   rw [divInt_mul_divInt _ _ this one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this]
 #align rat.mul_denom_eq_num Rat.mul_den_eq_num
 
-lemma den_mul_eq_num (q : ℚ) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num]
+@[simp] lemma den_mul_eq_num (q : ℚ) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num]
 
 -- 2024-04-05
 @[deprecated] alias coe_int_eq_divInt := intCast_eq_divInt