feat(data/rat): add @[simp] to rat.num_div_denom (#7393)

I have an equation in rational numbers that I want to turn into an equation in integers, and everything `simp`s away nicely except the equation `x.num / x.denom = x`. Marking `rat.num_div_denom` as `simp` should fix that, and I don't expect it will break anything. (`rat.num_denom : rat.mk x.num x.denom = x` is already a `simp` lemma.)

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60x.2Enum.20.2F.20x.2Edenom.20.3D.20x.60

archive/imo/imo2013_q5.lean

@@ -292,7 +292,7 @@ begin
   have hx2cnezr : (x2denom : ℝ) ≠ (0 : ℝ) := nat.cast_ne_zero.mpr (ne_of_gt hx2pos),
 
   have hrat_expand2 := calc x = x.num / x.denom : by exact_mod_cast rat.num_denom.symm
-                          ... = x2num / x2denom : by { field_simp, linarith [hxcnez] },
+                          ... = x2num / x2denom : by { field_simp [-rat.num_div_denom], linarith },
 
   have h_denom_times_fx :=
     calc (x2denom : ℝ) * f x = f (x2denom * x)                 : (h_f_commutes_with_pos_nat_mul

src/data/rat/basic.lean

@@ -609,6 +609,7 @@ begin
   simp [division_def, coe_int_eq_mk, mul_def one_ne_zero d0]
 end
 
+@[simp]
 theorem num_div_denom (r : ℚ) : (r.num / r.denom : ℚ) = r :=
 by rw [← int.cast_coe_nat, ← mk_eq_div, num_denom]
 

src/number_theory/pythagorean_triples.lean

@@ -435,17 +435,19 @@ begin
   let m := (q.denom : ℤ),
   let n := q.num,
   have hm0 : m ≠ 0, { norm_cast, apply rat.denom_ne_zero q },
-  have hq2 : q = n / m, { rw [int.cast_coe_nat], exact (rat.cast_id q).symm },
+  have hq2 : q = n / m := (rat.num_div_denom q).symm,
   have hm2n2 : 0 < m ^ 2 + n ^ 2,
   { apply lt_add_of_pos_of_le _ (sq_nonneg n),
     exact lt_of_le_of_ne (sq_nonneg m) (ne.symm (pow_ne_zero 2 hm0)) },
   have hw2 : w = (m ^ 2 - n ^ 2) / (m ^ 2 + n ^ 2),
-  { rw [ht4.2, hq2], field_simp [hm2n2, (rat.denom_ne_zero q)] },
+  { rw [ht4.2, hq2], field_simp [hm2n2, rat.denom_ne_zero q, -rat.num_div_denom] },
   have hm2n20 : (m : ℚ) ^ 2 + (n : ℚ) ^ 2 ≠ 0,
   { norm_cast, simpa only [int.coe_nat_pow] using ne_of_gt hm2n2 },
   have hv2 : v = 2 * m * n / (m ^ 2 + n ^ 2),
   { apply eq.symm, apply (div_eq_iff hm2n20).mpr, rw [ht4.1], field_simp [hQ q],
-    rw [hq2] {occs := occurrences.pos [2, 3]}, field_simp [rat.denom_ne_zero q], ring },
+    rw [hq2] {occs := occurrences.pos [2, 3]},
+    field_simp [rat.denom_ne_zero q, -rat.num_div_denom],
+    ring },
   have hnmcp : int.gcd n m = 1 := q.cop,
   have hmncp : int.gcd m n = 1, { rw int.gcd_comm, exact hnmcp },
   cases int.mod_two_eq_zero_or_one m with hm2 hm2;