chore(*) add mod_add_div' and div_add_mod' and golf proofs (#5962)

Resolves issue #1534.

Name of nat.mod_add_div shouldn't be changed as this is in core. Better name suggestions for mod_add_div' and div_add_mod' welcome.



Co-authored-by: Julian <kuelsha@mathematik.uni-stuttgart.de>

archive/imo/imo1962_q1.lean

@@ -43,7 +43,7 @@ begin
   { rw [problem_predicate, digits_def' (dec_trivial : 2 ≤ 10) n.succ_pos,
         list.head, list.tail_cons, list.concat_eq_append] at h1,
     split,
-    { rw [← h1.left, add_comm, mod_add_div (n+1) 10], },
+    { rw [← h1.left, div_add_mod (n+1) 10], },
     { rw [← h1.right, of_digits_append, of_digits_digits,
           of_digits_singleton, add_comm, mul_comm], }, },
 end

archive/imo/imo1964_q1.lean

@@ -63,7 +63,7 @@ begin
   split,
   { intro h,
     let t := n % 3,
-    rw [(show n = t + 3 * (n / 3), from (nat.mod_add_div n 3).symm), add_comm] at h,
+    rw [(show n = 3 * (n / 3) + t, from (nat.div_add_mod n 3).symm)] at h,
     have ht : t < 3 := nat.mod_lt _ dec_trivial,
     interval_cases t with hr; rw hr at h,
     { exact nat.dvd_of_mod_eq_zero hr },
@@ -82,22 +82,20 @@ end
 theorem imo1964_q1b (n : ℕ) : ¬ (7 ∣ 2 ^ n + 1) :=
 begin
   let t := n % 3,
-  rw [← modeq_zero_iff, (show n = t + 3 * (n / 3), from (nat.mod_add_div n 3).symm), add_comm],
+  rw [← modeq_zero_iff, (show n = 3 * (n / 3) + t, from (nat.div_add_mod n 3).symm)],
   have ht : t < 3 := nat.mod_lt _ dec_trivial,
   interval_cases t with hr; rw hr,
-  { rw zero_add,
+  { rw add_zero,
     intro h,
-    have := h.symm.trans (modeq_add (nat.modeq.refl _) (two_pow_three_mul_mod_seven _)),
+    have := h.symm.trans (modeq_add (two_pow_three_mul_mod_seven _) (nat.modeq.refl _)),
     rw modeq_iff_dvd at this,
     norm_num at this },
-  { rw add_comm _ (3 * _),
-    intro h,
-    have := h.symm.trans (modeq_add (nat.modeq.refl _) (two_pow_three_mul_add_one_mod_seven _)),
+  { intro h,
+    have := h.symm.trans (modeq_add (two_pow_three_mul_add_one_mod_seven _) (nat.modeq.refl _)),
     rw modeq_iff_dvd at this,
     norm_num at this },
-  { rw add_comm _ (3 * _),
-    intro h,
-    have := h.symm.trans (modeq_add (nat.modeq.refl _) (two_pow_three_mul_add_two_mod_seven _)),
+  { intro h,
+    have := h.symm.trans (modeq_add (two_pow_three_mul_add_two_mod_seven _) (nat.modeq.refl _)),
     rw modeq_iff_dvd at this,
     norm_num at this },
 end

src/algebra/euclidean_domain.lean

@@ -23,8 +23,6 @@ class euclidean_domain (R : Type u) extends comm_ring R, nontrivial R :=
 (quotient : R → R → R)
 (quotient_zero : ∀ a, quotient a 0 = 0)
 (remainder : R → R → R)
- -- This could be changed to the same order as int.mod_add_div.
- -- We normally write `qb+r` rather than `r + qb` though.
 (quotient_mul_add_remainder_eq : ∀ a b, b * quotient a b + remainder a b = a)
 (r : R → R → Prop)
 (r_well_founded : well_founded r)
@@ -50,6 +48,12 @@ euclidean_domain.quotient_mul_add_remainder_eq _ _
 lemma mod_add_div (a b : R) : a % b + b * (a / b) = a :=
 (add_comm _ _).trans (div_add_mod _ _)
 
+lemma mod_add_div' (m k : R) : m % k + (m / k) * k = m :=
+by { rw mul_comm, exact mod_add_div _ _ }
+
+lemma div_add_mod' (m k : R) : (m / k) * k + m % k = m :=
+by { rw mul_comm, exact div_add_mod _ _ }
+
 lemma mod_eq_sub_mul_div {R : Type*} [euclidean_domain R] (a b : R) :
   a % b = a - b * (a / b) :=
 calc a % b = b * (a / b) + a % b - b * (a / b) : (add_sub_cancel' _ _).symm
@@ -358,7 +362,7 @@ instance int.euclidean_domain : euclidean_domain ℤ :=
   quotient := (/),
   quotient_zero := int.div_zero,
   remainder := (%),
-  quotient_mul_add_remainder_eq := λ a b, by rw add_comm; exact int.mod_add_div _ _,
+  quotient_mul_add_remainder_eq := λ a b, int.div_add_mod _ _,
   r := λ a b, a.nat_abs < b.nat_abs,
   r_well_founded := measure_wf (λ a, int.nat_abs a),
   remainder_lt := λ a b b0, int.coe_nat_lt.1 $

src/data/int/basic.lean

@@ -479,6 +479,12 @@ theorem mod_add_div : ∀ (a b : ℤ), a % b + b * (a / b) = a
 theorem div_add_mod (a b : ℤ) : b * (a / b) + a % b = a :=
 (add_comm _ _).trans (mod_add_div _ _)
 
+lemma mod_add_div' (m k : ℤ) : m % k + (m / k) * k = m :=
+by { rw mul_comm, exact mod_add_div _ _ }
+
+lemma div_add_mod' (m k : ℤ) : (m / k) * k + m % k = m :=
+by { rw mul_comm, exact div_add_mod _ _ }
+
 theorem mod_def (a b : ℤ) : a % b = a - b * (a / b) :=
 eq_sub_of_add_eq (mod_add_div _ _)
 
@@ -540,9 +546,9 @@ by rw [mul_comm, mul_mod_left]
 lemma mul_mod (a b n : ℤ) : (a * b) % n = ((a % n) * (b % n)) % n :=
 begin
   conv_lhs {
-    rw [←mod_add_div a n, ←mod_add_div b n, right_distrib, left_distrib, left_distrib,
-        mul_assoc, mul_assoc, ←left_distrib n _ _, add_mul_mod_self_left,
-        mul_comm _ (n * (b / n)), mul_assoc, add_mul_mod_self_left] }
+    rw [←mod_add_div a n, ←mod_add_div' b n, right_distrib, left_distrib, left_distrib,
+        mul_assoc, mul_assoc, ←left_distrib n _ _, add_mul_mod_self_left, ← mul_assoc,
+        add_mul_mod_self] }
 end
 
 @[simp] lemma neg_mod_two (i : ℤ) : (-i) % 2 = i % 2 :=

src/data/nat/basic.lean

@@ -833,6 +833,15 @@ by rw [mul_comm,nat.div_mul_cancel Hd]
 
 /-! ### `mod`, `dvd` -/
 
+lemma div_add_mod (m k : ℕ) : k * (m / k) + m % k = m :=
+(nat.add_comm _ _).trans (mod_add_div _ _)
+
+lemma mod_add_div' (m k : ℕ) : m % k + (m / k) * k = m :=
+by { rw mul_comm, exact mod_add_div _ _ }
+
+lemma div_add_mod' (m k : ℕ) : (m / k) * k + m % k = m :=
+by { rw mul_comm, exact div_add_mod _ _ }
+
 protected theorem div_mod_unique {n k m d : ℕ} (h : 0 < k) :
   n / k = d ∧ n % k = m ↔ m + k * d = n ∧ m < k :=
 ⟨λ ⟨e₁, e₂⟩, e₁ ▸ e₂ ▸ ⟨mod_add_div _ _, mod_lt _ h⟩,
@@ -979,9 +988,9 @@ by rw [add_comm, add_mod_eq_add_mod_right _ H, add_comm]
 lemma mul_mod (a b n : ℕ) : (a * b) % n = ((a % n) * (b % n)) % n :=
 begin
   conv_lhs {
-    rw [←mod_add_div a n, ←mod_add_div b n, right_distrib, left_distrib, left_distrib,
-        mul_assoc, mul_assoc, ←left_distrib n _ _, add_mul_mod_self_left,
-        mul_comm _ (n * (b / n)), mul_assoc, add_mul_mod_self_left] }
+    rw [←mod_add_div a n, ←mod_add_div' b n, right_distrib, left_distrib, left_distrib,
+        mul_assoc, mul_assoc, ←left_distrib n _ _, add_mul_mod_self_left, ← mul_assoc,
+        add_mul_mod_self_right] }
 end
 
 lemma dvd_div_of_mul_dvd {a b c : ℕ} (h : a * b ∣ c) : b ∣ c / a :=
@@ -1175,7 +1184,7 @@ begin
     { rw [div_lt_iff_lt_mul p _ b_pos],
       simpa [pow_succ'] using h₁ },
     rw [mod_eq_of_lt h₁, mod_eq_of_lt h₂],
-    simp [mod_add_div, nat.add_comm] },
+    simp [div_add_mod] },
   -- step: p ≥ b^succ w
   { -- Generate condition for induction hypothesis
     have h₂ : p - b^succ w < p,

src/data/nat/fib.lean

@@ -152,8 +152,8 @@ begin
     { simp },
     intros m n mpos h,
     rw ← gcd_rec m n at h,
-    conv_rhs { rw ← mod_add_div n m },
-    rwa [mul_comm, gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _] },
+    conv_rhs { rw ← mod_add_div' n m },
+    rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _] },
   rwa [gcd_comm, gcd_comm (fib m)]
 end
 

src/data/pnat/basic.lean

@@ -292,6 +292,12 @@ end
 theorem div_add_mod (m k : ℕ+) : (k * (div m k) + mod m k : ℕ) = m :=
 (add_comm _ _).trans (mod_add_div _ _)
 
+lemma mod_add_div' (m k : ℕ+) : ((mod m k) + (div m k) * k : ℕ) = m :=
+by { rw mul_comm, exact mod_add_div _ _ }
+
+lemma div_add_mod' (m k : ℕ+) : ((div m k) * k + mod m k : ℕ) = m :=
+by { rw mul_comm, exact div_add_mod _ _ }
+
 theorem mod_coe (m k : ℕ+) :
  ((mod m k) : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ)) :=
 begin
@@ -354,7 +360,7 @@ theorem mul_div_exact {m k : ℕ+} (h : k ∣ m) : k * (div_exact m k) = m :=
 begin
  apply eq, rw [mul_coe],
  change (k : ℕ) * (div m k).succ = m,
- rw [← mod_add_div m k, dvd_iff'.mp h, nat.mul_succ, add_comm],
+ rw [← div_add_mod m k, dvd_iff'.mp h, nat.mul_succ]
 end
 
 theorem dvd_antisymm {m n : ℕ+} : m ∣ n → n ∣ m → m = n :=

src/number_theory/lucas_lehmer.lean

@@ -505,9 +505,9 @@ Someone should do this, too!
 lemma modeq_mersenne (n k : ℕ) : k ≡ ((k / 2^n) + (k % 2^n)) [MOD 2^n - 1] :=
 -- See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help.20finding.20a.20lemma/near/177698446
 begin
-  conv in k {rw [← nat.mod_add_div k (2^n), add_comm]},
+  conv in k { rw ← nat.div_add_mod k (2^n) },
   refine nat.modeq.modeq_add _ (by refl),
-  conv {congr, skip, skip, rw ← one_mul (k/2^n)},
+  conv { congr, skip, skip, rw ← one_mul (k/2^n) },
   refine nat.modeq.modeq_mul _ (by refl),
   symmetry,
   rw [nat.modeq.modeq_iff_dvd, int.coe_nat_sub],

src/number_theory/quadratic_reciprocity.lean

@@ -440,7 +440,7 @@ have hx2 : ∀ x ∈ Ico 1 (p / 2).succ, (2 * x : zmod p).val = 2 * x,
   from λ x hx, have h2xp : 2 * x < p,
       from calc 2 * x ≤ 2 * (p / 2) : mul_le_mul_of_nonneg_left
         (le_of_lt_succ $ by finish) dec_trivial
-      ... < _ : by conv_rhs {rw [← mod_add_div p 2, add_comm, show p % 2 = 1, from hp1]}; exact lt_succ_self _,
+      ... < _ : by conv_rhs {rw [← div_add_mod p 2, show p % 2 = 1, from hp1]}; exact lt_succ_self _,
     by rw [← nat.cast_two, ← nat.cast_mul, val_cast_of_lt h2xp],
 have hdisj : disjoint
     ((Ico 1 (p / 2).succ).filter (λ x, p / 2 < ((2 : ℕ) * x : zmod p).val))

src/set_theory/ordinal_arithmetic.lean

@@ -1344,7 +1344,7 @@ le_antisymm
 
 @[simp] theorem nat_cast_mod {m n : ℕ} : ((m % n : ℕ) : ordinal) = m % n :=
 by rw [← add_left_cancel (n*(m/n)), div_add_mod, ← nat_cast_div, ← nat_cast_mul, ← nat.cast_add,
-       add_comm, nat.mod_add_div]
+       nat.div_add_mod]
 
 @[simp] theorem nat_le_card {o} {n : ℕ} : (n : cardinal) ≤ card o ↔ (n : ordinal) ≤ o :=
 ⟨λ h, by rwa [← cardinal.ord_le, cardinal.ord_nat] at h,