feat(data/int/cast): int cast division lemmas (#13929)

Adds lemmas for passing int cast through division, and renames the nat versions from `nat.cast_dvd` to `nat.cast_div`. 
Also some golf.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/char_zero.lean

@@ -101,13 +101,12 @@ lemma cast_add_one_ne_zero (n : ℕ) : (n + 1 : R) ≠ 0 :=
 by exact_mod_cast n.succ_ne_zero
 
 @[simp, norm_cast]
-theorem cast_dvd_char_zero {k : Type*} [field k] [char_zero k] {m n : ℕ}
+theorem cast_div_char_zero {k : Type*} [field k] [char_zero k] {m n : ℕ}
   (n_dvd : n ∣ m) : ((m / n : ℕ) : k) = m / n :=
 begin
-  by_cases hn : n = 0,
-  { subst hn,
-    simp },
-  { exact cast_dvd n_dvd (cast_ne_zero.mpr hn), },
+  rcases eq_or_ne n 0 with rfl | hn,
+  { simp },
+  { exact cast_div n_dvd (cast_ne_zero.2 hn), },
 end
 
 end nat

src/data/int/cast.lean

@@ -111,6 +111,14 @@ by simp [sub_eq_add_neg]
 | -[1+ m] -[1+ n] := show (((m + 1) * (n + 1) : ℕ) : α) = -(m + 1) * -(n + 1),
   by rw [nat.cast_mul, nat.cast_add_one, nat.cast_add_one, neg_mul_neg]
 
+@[simp] theorem cast_div [field α] {m n : ℤ} (n_dvd : n ∣ m) (n_nonzero : (n : α) ≠ 0) :
+  ((m / n : ℤ) : α) = m / n :=
+begin
+  rcases n_dvd with ⟨k, rfl⟩,
+  have : n ≠ 0, { rintro rfl, simpa using n_nonzero },
+  rw [int.mul_div_cancel_left _ this, int.cast_mul, mul_div_cancel_left _ n_nonzero],
+end
+
 /-- `coe : ℤ → α` as an `add_monoid_hom`. -/
 def cast_add_hom (α : Type*) [add_group α] [has_one α] : ℤ →+ α := ⟨coe, cast_zero, cast_add⟩
 

src/data/int/char_zero.lean

@@ -35,6 +35,15 @@ theorem cast_injective [add_group α] [has_one α] [char_zero α] : function.inj
 theorem cast_ne_zero [add_group α] [has_one α] [char_zero α] {n : ℤ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
 not_congr cast_eq_zero
 
+@[simp, norm_cast]
+theorem cast_div_char_zero {k : Type*} [field k] [char_zero k] {m n : ℤ}
+  (n_dvd : n ∣ m) : ((m / n : ℤ) : k) = m / n :=
+begin
+  rcases eq_or_ne n 0 with rfl | hn,
+  { simp [int.div_zero] },
+  { exact cast_div n_dvd (cast_ne_zero.mpr hn), },
+end
+
 end int
 
 lemma ring_hom.injective_int {α : Type*} [ring α] (f : ℤ →+* α) [char_zero α] :

src/data/nat/cast.lean

@@ -132,13 +132,12 @@ eq_sub_of_add_eq $ by rw [← cast_add, tsub_add_cancel_of_le h]
 | (n+1) := (cast_add _ _).trans $
 show ((m * n : ℕ) : α) + m = m * (n + 1), by rw [cast_mul n, left_distrib, mul_one]
 
-@[simp] theorem cast_dvd {α : Type*} [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n:α) ≠ 0) :
+@[simp] theorem cast_div [field α] {m n : ℕ} (n_dvd : n ∣ m) (n_nonzero : (n : α) ≠ 0) :
   ((m / n : ℕ) : α) = m / n :=
 begin
   rcases n_dvd with ⟨k, rfl⟩,
   have : n ≠ 0, {rintro rfl, simpa using n_nonzero},
-  rw nat.mul_div_cancel_left _ (pos_iff_ne_zero.2 this),
-  rw [nat.cast_mul, mul_div_cancel_left _ n_nonzero],
+  rw [nat.mul_div_cancel_left _ this.bot_lt, cast_mul, mul_div_cancel_left _ n_nonzero],
 end
 
 /-- `coe : ℕ → α` as a `ring_hom` -/

src/data/nat/totient.lean

@@ -335,7 +335,7 @@ begin
   { rw [←cast_prod, cast_ne_zero, ←zero_lt_iff, ←prod_factorization_eq_prod_factors],
     exact prod_pos (λ p hp, pos_of_mem_factorization hp) },
   simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod,
-      cast_dvd_char_zero, mul_comm_div', mul_right_inj' hn', div_eq_iff hpQ, ←prod_mul_distrib],
+      cast_div_char_zero, mul_comm_div', mul_right_inj' hn', div_eq_iff hpQ, ←prod_mul_distrib],
   refine prod_congr rfl (λ p hp, _),
   have hp := pos_of_mem_factors (list.mem_to_finset.mp hp),
   have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm,

src/number_theory/bernoulli.lean

@@ -148,7 +148,7 @@ begin
   have := factorial_mul_factorial_dvd_factorial_add i j,
   field_simp [mul_comm _ (bernoulli' i), mul_assoc, add_choose],
   rw_mod_cast [mul_comm (j + 1), mul_div_assoc, ← mul_assoc],
-  rw [cast_mul, cast_mul, mul_div_mul_right, cast_dvd_char_zero, cast_mul],
+  rw [cast_mul, cast_mul, mul_div_mul_right, cast_div_char_zero, cast_mul],
   assumption',
 end
 
@@ -256,7 +256,7 @@ begin
   have hj : (j.succ : ℚ) ≠ 0 := by exact_mod_cast succ_ne_zero j,
   field_simp [← h, mul_ne_zero hj (hfact j), hfact i, mul_comm _ (bernoulli i), mul_assoc],
   rw_mod_cast [mul_comm (j + 1), mul_div_assoc, ← mul_assoc],
-  rw [cast_mul, cast_mul, mul_div_mul_right _ _ hj, add_choose, cast_dvd_char_zero],
+  rw [cast_mul, cast_mul, mul_div_mul_right _ _ hj, add_choose, cast_div_char_zero],
   apply factorial_mul_factorial_dvd_factorial_add,
 end
 
@@ -287,7 +287,7 @@ begin
     rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one,
         mul_assoc _ _ ↑q.succ!, mul_comm _ ↑q.succ!, ← mul_assoc, div_mul_eq_mul_div,
         mul_comm (↑n ^ (q - m + 1)), ← mul_assoc _ _ (↑n ^ (q - m + 1)), ← one_div, mul_one_div,
-        div_div_eq_div_mul, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_dvd, cast_mul],
+        div_div_eq_div_mul, tsub_add_eq_add_tsub (le_of_lt_succ h), cast_div, cast_mul],
     { ring },
     { exact factorial_mul_factorial_dvd_factorial h.le },
     { simp [hne] } },

src/number_theory/von_mangoldt.lean

@@ -124,7 +124,7 @@ begin
     { rw [cast_ne_zero],
       rintro rfl,
       exact hn (by simpa using mn) },
-    rw [nat.cast_dvd mn this, real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub] },
+    rw [nat.cast_div mn this, real.log_div (cast_ne_zero.2 hn) this, neg_sub, mul_sub] },
   rw [this, sum_sub_distrib, ←sum_mul, ←int.cast_sum, ←coe_mul_zeta_apply, eq_comm, sub_eq_self,
     moebius_mul_coe_zeta, mul_eq_zero, int.cast_eq_zero],
   rcases eq_or_ne n 1 with hn | hn;

src/ring_theory/discriminant.lean

@@ -203,7 +203,7 @@ begin
   have hle : 1 ≤ pb.dim,
   { rw [← hn, nat.one_le_iff_ne_zero, ← zero_lt_iff, finite_dimensional.finrank_pos_iff],
     apply_instance },
-  rw [hn, nat.cast_dvd h₂ hne, nat.cast_mul, nat.cast_sub hle],
+  rw [hn, nat.cast_div h₂ hne, nat.cast_mul, nat.cast_sub hle],
   field_simp,
   ring,
 end

src/ring_theory/power_series/well_known.lean

@@ -110,7 +110,7 @@ begin
   symmetry,
   rw [div_eq_iff, div_mul_eq_mul_div, one_mul, choose_eq_factorial_div_factorial],
   norm_cast,
-  rw cast_dvd_char_zero,
+  rw cast_div_char_zero,
   { apply factorial_mul_factorial_dvd_factorial (mem_range_succ_iff.1 hx), },
   { apply mem_range_succ_iff.1 hx, },
   { rintros h, apply factorial_ne_zero n, rw cast_eq_zero.1 h, },