feat(data/rat/basic): API around rat.mk (#10782)

src/data/rat/basic.lean

@@ -72,6 +72,12 @@ instance : has_zero ℚ := ⟨of_int 0⟩
 instance : has_one ℚ := ⟨of_int 1⟩
 instance : inhabited ℚ := ⟨0⟩
 
+lemma ext_iff {p q : ℚ} : p = q ↔ p.num = q.num ∧ p.denom = q.denom :=
+by { cases p, cases q, simp }
+
+@[ext] lemma ext {p q : ℚ} (hn : p.num = q.num) (hd : p.denom = q.denom) : p = q :=
+rat.ext_iff.mpr ⟨hn, hd⟩
+
 /-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ+` (not necessarily coprime) -/
 def mk_pnat (n : ℤ) : ℕ+ → ℚ | ⟨d, dpos⟩ :=
 let n' := n.nat_abs, g := n'.gcd d in
@@ -304,6 +310,12 @@ begin
   simp only [neg_mul_eq_neg_mul_symm, congr_arg has_neg.neg h₁]
 end
 
+@[simp] lemma mk_neg_denom (n d : ℤ) : n /. -d = -n /. d :=
+begin
+  by_cases hd : d = 0;
+  simp [rat.mk_eq, hd]
+end
+
 /-- Multiplication of rational numbers. Use `(*)` instead. -/
 protected def mul : ℚ → ℚ → ℚ
 | ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * n₂) ⟨d₁ * d₂, mul_pos h₁ h₂⟩
@@ -562,6 +574,28 @@ theorem mk_pnat_denom (n : ℤ) (d : ℕ+) :
   (mk_pnat n d).denom = d / nat.gcd n.nat_abs d :=
 by cases d; refl
 
+lemma num_mk (n d : ℤ) :
+  (n /. d).num = d.sign * n / n.gcd d :=
+begin
+  rcases d with ((_ | _) | _),
+  { simp },
+  { simpa [←int.coe_nat_succ, int.sign_coe_nat_of_nonzero] },
+  { rw rat.mk,
+    simpa [rat.mk_pnat_num, int.neg_succ_of_nat_eq, ←int.coe_nat_succ,
+           int.sign_coe_nat_of_nonzero] }
+end
+
+lemma denom_mk (n d : ℤ) :
+  (n /. d).denom = if d = 0 then 1 else d.nat_abs / n.gcd d :=
+begin
+  rcases d with ((_ | _) | _),
+  { simp },
+  { simpa [←int.coe_nat_succ, int.sign_coe_nat_of_nonzero] },
+  { rw rat.mk,
+    simpa [rat.mk_pnat_denom, int.neg_succ_of_nat_eq, ←int.coe_nat_succ,
+           int.sign_coe_nat_of_nonzero] }
+end
+
 theorem mk_pnat_denom_dvd (n : ℤ) (d : ℕ+) :
   (mk_pnat n d).denom ∣ d.1 :=
 begin

src/number_theory/bernoulli.lean

@@ -202,7 +202,7 @@ begin
   have f := sum_bernoulli' n.succ.succ,
   simp_rw [sum_range_succ', bernoulli'_one, choose_one_right, cast_succ, ← eq_sub_iff_add_eq] at f,
   convert f,
-  { ext x, rw bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj) },
+  { funext x, rw bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj) },
   { simp only [one_div, mul_one, bernoulli'_zero, cast_one, choose_zero_right, add_sub_cancel],
     ring },
 end
@@ -275,7 +275,7 @@ begin
   have h_cauchy : mk (λ p, bernoulli p / p!) * mk (λ q, coeff ℚ (q + 1) (exp ℚ ^ n))
                 = mk (λ p, ∑ i in range (p + 1),
                       bernoulli i * (p + 1).choose i * n ^ (p + 1 - i) / (p + 1)!),
-  { ext q,
+  { ext q : 1,
     let f := λ a b, bernoulli a / a! * coeff ℚ (b + 1) (exp ℚ ^ n),
     -- key step: use `power_series.coeff_mul` and then rewrite sums
     simp only [coeff_mul, coeff_mk, cast_mul, sum_antidiagonal_eq_sum_range_succ f],

src/number_theory/number_field.lean

@@ -102,7 +102,7 @@ instance rat.number_field : number_field ℚ :=
              -- all fields are vector spaces over themselves (used in `rat.finite_dimensional`)
              -- all char 0 fields have a canonical embedding of `ℚ` (used in `number_field`).
              -- Show that these coincide:
-             ext, simp [algebra.smul_def] } }
+             ext1, simp [algebra.smul_def] } }
 
 /-- The ring of integers of `ℚ` as a number field is just `ℤ`. -/
 noncomputable def ring_of_integers_equiv : ring_of_integers ℚ ≃+* ℤ :=