From 13b4f95f926bf6089125932038525657ffcb9ccc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 9 May 2024 08:48:29 +0100 Subject: [PATCH] make simp --- Mathlib/Data/NNRat/Defs.lean | 4 ++-- Mathlib/Data/Rat/Defs.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean index 18e6f0c0dc5e6..79eb0c1ba042b 100644 --- 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 index 66434dec9d36d..d9c55a22faa14 100644 --- 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