chore(Data/Nat/Factorial): Use Std lemmas (#11715)

Make use of `Nat`-specific lemmas from Std rather than the general ones provided by mathlib.

The ultimate goal here is to carve out `Data`, `Algebra` and `Order` sublibraries.

Author: YaelDillies

Archive/Imo/Imo2019Q4.lean

@@ -3,9 +3,9 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.Tactic.IntervalCases
-import Mathlib.Algebra.BigOperators.Order
+import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Multiplicity
+import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.GCongr
 
 #align_import imo.imo2019_q4 from "leanprover-community/mathlib"@"308826471968962c6b59c7ff82a22757386603e3"

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -604,7 +604,7 @@ end ENNReal
 
 
 theorem factorial_tendsto_atTop : Tendsto Nat.factorial atTop atTop :=
-  tendsto_atTop_atTop_of_monotone Nat.monotone_factorial fun n ↦ ⟨n, n.self_le_factorial⟩
+  tendsto_atTop_atTop_of_monotone (fun _ _ ↦ Nat.factorial_le) fun n ↦ ⟨n, n.self_le_factorial⟩
 #align factorial_tendsto_at_top factorial_tendsto_atTop
 
 theorem tendsto_factorial_div_pow_self_atTop :

Mathlib/Data/Nat/Choose/Basic.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Bhavik Mehta, Stuart Presnell
 -/
 import Mathlib.Data.Nat.Factorial.Basic
-import Mathlib.Algebra.Divisibility.Basic
-import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Order.Monotone.Basic
 
 #align_import data.nat.choose.basic from "leanprover-community/mathlib"@"2f3994e1b117b1e1da49bcfb67334f33460c3ce4"
 
@@ -87,12 +86,12 @@ theorem choose_succ_self (n : ℕ) : choose n (succ n) = 0 :=
 #align nat.choose_succ_self Nat.choose_succ_self
 
 @[simp]
-theorem choose_one_right (n : ℕ) : choose n 1 = n := by induction n <;> simp [*, choose, add_comm]
+lemma choose_one_right (n : ℕ) : choose n 1 = n := by induction n <;> simp [*, choose, Nat.add_comm]
 #align nat.choose_one_right Nat.choose_one_right
 
 -- The `n+1`-st triangle number is `n` more than the `n`-th triangle number
 theorem triangle_succ (n : ℕ) : (n + 1) * (n + 1 - 1) / 2 = n * (n - 1) / 2 + n := by
-  rw [← add_mul_div_left, mul_comm 2 n, ← mul_add, Nat.add_sub_cancel, mul_comm]
+  rw [← add_mul_div_left, Nat.mul_comm 2 n, ← Nat.mul_add, Nat.add_sub_cancel, Nat.mul_comm]
   cases n <;> rfl; apply zero_lt_succ
 #align nat.triangle_succ Nat.triangle_succ
 
@@ -101,7 +100,7 @@ theorem choose_two_right (n : ℕ) : choose n 2 = n * (n - 1) / 2 := by
   induction' n with n ih
   · simp
   · rw [triangle_succ n, choose, ih]
-    simp [add_comm]
+    simp [Nat.add_comm]
 #align nat.choose_two_right Nat.choose_two_right
 
 theorem choose_pos : ∀ {n k}, k ≤ n → 0 < choose n k
@@ -117,10 +116,10 @@ theorem choose_eq_zero_iff {n k : ℕ} : n.choose k = 0 ↔ n < k :=
 theorem succ_mul_choose_eq : ∀ n k, succ n * choose n k = choose (succ n) (succ k) * succ k
   | 0, 0 => by decide
   | 0, k + 1 => by simp [choose]
-  | n + 1, 0 => by simp [choose, mul_succ, succ_eq_add_one, add_comm]
+  | n + 1, 0 => by simp [choose, mul_succ, succ_eq_add_one, Nat.add_comm]
   | n + 1, k + 1 => by
-    rw [choose_succ_succ (succ n) (succ k), add_mul, ← succ_mul_choose_eq n, mul_succ, ←
-      succ_mul_choose_eq n, add_right_comm, ← mul_add, ← choose_succ_succ, ← succ_mul]
+    rw [choose_succ_succ (succ n) (succ k), Nat.add_mul, ← succ_mul_choose_eq n, mul_succ, ←
+      succ_mul_choose_eq n, Nat.add_right_comm, ← Nat.mul_add, ← choose_succ_succ, ← succ_mul]
 #align nat.succ_mul_choose_eq Nat.succ_mul_choose_eq
 
 theorem choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k * k ! * (n - k)! = n !
@@ -130,56 +129,57 @@ theorem choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k *
     rcases lt_or_eq_of_le hk with hk₁ | hk₁
     · have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
         rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
-        simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
+        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
       have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
         rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
       have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
         rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
-        simp [factorial_succ, mul_comm, mul_left_comm, mul_assoc]
+        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
       have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
-      rw [choose_succ_succ, add_mul, add_mul, succ_sub_succ, h, h₁, h₂, add_mul,
-        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, add_assoc, ← add_mul,
-        Nat.add_sub_cancel_left, add_comm]
-    · rw [hk₁]; simp [hk₁, mul_comm, choose, Nat.sub_self]
+      rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
+        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
+        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]
+    · rw [hk₁]; simp [hk₁, Nat.mul_comm, choose, Nat.sub_self]
 #align nat.choose_mul_factorial_mul_factorial Nat.choose_mul_factorial_mul_factorial
 
 theorem choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
     n.choose k * k.choose s = n.choose s * (n - s).choose (k - s) :=
-  have h : (n - k)! * (k - s)! * s ! ≠ 0 := by apply_rules [factorial_ne_zero, mul_ne_zero]
-  mul_right_cancel₀ h <|
+  have h : 0 < (n - k)! * (k - s)! * s ! := by apply_rules [factorial_pos, Nat.mul_pos]
+  Nat.mul_right_cancel h <|
   calc
     n.choose k * k.choose s * ((n - k)! * (k - s)! * s !) =
         n.choose k * (k.choose s * s ! * (k - s)!) * (n - k)! :=
-      by rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc _ s !, mul_assoc, mul_comm (n - k)!,
-        mul_comm s !]
+      by rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc, Nat.mul_assoc _ s !, Nat.mul_assoc,
+        Nat.mul_comm (n - k)!, Nat.mul_comm s !]
     _ = n ! :=
       by rw [choose_mul_factorial_mul_factorial hsk, choose_mul_factorial_mul_factorial hkn]
     _ = n.choose s * s ! * ((n - s).choose (k - s) * (k - s)! * (n - s - (k - s))!) :=
       by rw [choose_mul_factorial_mul_factorial (Nat.sub_le_sub_right hkn _),
         choose_mul_factorial_mul_factorial (hsk.trans hkn)]
     _ = n.choose s * (n - s).choose (k - s) * ((n - k)! * (k - s)! * s !) := by
-      rw [Nat.sub_sub_sub_cancel_right hsk, mul_assoc, mul_left_comm s !, mul_assoc,
-        mul_comm (k - s)!, mul_comm s !, mul_right_comm, ← mul_assoc]
+      rw [Nat.sub_sub_sub_cancel_right hsk, Nat.mul_assoc, Nat.mul_left_comm s !, Nat.mul_assoc,
+        Nat.mul_comm (k - s)!, Nat.mul_comm s !, Nat.mul_right_comm, ← Nat.mul_assoc]
 #align nat.choose_mul Nat.choose_mul
 
 theorem choose_eq_factorial_div_factorial {n k : ℕ} (hk : k ≤ n) :
     choose n k = n ! / (k ! * (n - k)!) := by
-  rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]
+  rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]
   exact (mul_div_left _ (Nat.mul_pos (factorial_pos _) (factorial_pos _))).symm
 #align nat.choose_eq_factorial_div_factorial Nat.choose_eq_factorial_div_factorial
 
 theorem add_choose (i j : ℕ) : (i + j).choose j = (i + j)! / (i ! * j !) := by
-  rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right, mul_comm]
+  rw [choose_eq_factorial_div_factorial (Nat.le_add_left j i), Nat.add_sub_cancel_right,
+    Nat.mul_comm]
 #align nat.add_choose Nat.add_choose
 
 theorem add_choose_mul_factorial_mul_factorial (i j : ℕ) :
     (i + j).choose j * i ! * j ! = (i + j)! := by
   rw [← choose_mul_factorial_mul_factorial (Nat.le_add_left _ _), Nat.add_sub_cancel_right,
-    mul_right_comm]
+    Nat.mul_right_comm]
 #align nat.add_choose_mul_factorial_mul_factorial Nat.add_choose_mul_factorial_mul_factorial
 
 theorem factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) : k ! * (n - k)! ∣ n ! := by
-  rw [← choose_mul_factorial_mul_factorial hk, mul_assoc]; exact dvd_mul_left _ _
+  rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]; exact Nat.dvd_mul_left _ _
 #align nat.factorial_mul_factorial_dvd_factorial Nat.factorial_mul_factorial_dvd_factorial
 
 theorem factorial_mul_factorial_dvd_factorial_add (i j : ℕ) : i ! * j ! ∣ (i + j)! := by
@@ -191,7 +191,7 @@ theorem factorial_mul_factorial_dvd_factorial_add (i j : ℕ) : i ! * j ! ∣ (i
 @[simp]
 theorem choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n - k) = choose n k := by
   rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (Nat.sub_le _ _),
-    Nat.sub_sub_self hk, mul_comm]
+    Nat.sub_sub_self hk, Nat.mul_comm]
 #align nat.choose_symm Nat.choose_symm
 
 theorem choose_symm_of_eq_add {n a b : ℕ} (h : n = a + b) : Nat.choose n a = Nat.choose n b := by
@@ -206,13 +206,13 @@ theorem choose_symm_add {a b : ℕ} : choose (a + b) a = choose (a + b) b :=
 
 theorem choose_symm_half (m : ℕ) : choose (2 * m + 1) (m + 1) = choose (2 * m + 1) m := by
   apply choose_symm_of_eq_add
-  rw [add_comm m 1, add_assoc 1 m m, add_comm (2 * m) 1, two_mul m]
+  rw [Nat.add_comm m 1, Nat.add_assoc 1 m m, Nat.add_comm (2 * m) 1, Nat.two_mul m]
 #align nat.choose_symm_half Nat.choose_symm_half
 
 theorem choose_succ_right_eq (n k : ℕ) : choose n (k + 1) * (k + 1) = choose n k * (n - k) := by
   have e : (n + 1) * choose n k = choose n (k + 1) * (k + 1) + choose n k * (k + 1) := by
-    rw [← right_distrib, add_comm (choose _ _), ← choose_succ_succ, succ_mul_choose_eq]
-  rw [← Nat.sub_eq_of_eq_add e, mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
+    rw [← Nat.add_mul, Nat.add_comm (choose _ _), ← choose_succ_succ, succ_mul_choose_eq]
+  rw [← Nat.sub_eq_of_eq_add e, Nat.mul_comm, ← Nat.mul_sub_left_distrib, Nat.add_sub_add_right]
 #align nat.choose_succ_right_eq Nat.choose_succ_right_eq
 
 @[simp]
@@ -226,63 +226,59 @@ theorem choose_mul_succ_eq (n k : ℕ) : n.choose k * (n + 1) = (n + 1).choose k
   | zero => simp
   | succ k =>
     obtain hk | hk := le_or_lt (k + 1) (n + 1)
-    · rw [choose_succ_succ, add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
+    · rw [choose_succ_succ, Nat.add_mul, succ_sub_succ, ← choose_succ_right_eq, ← succ_sub_succ,
         Nat.mul_sub_left_distrib, Nat.add_sub_cancel' (Nat.mul_le_mul_left _ hk)]
-    · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), zero_mul,
-        zero_mul]
+    · rw [choose_eq_zero_of_lt hk, choose_eq_zero_of_lt (n.lt_succ_self.trans hk), Nat.zero_mul,
+        Nat.zero_mul]
 #align nat.choose_mul_succ_eq Nat.choose_mul_succ_eq
 
 theorem ascFactorial_eq_factorial_mul_choose (n k : ℕ) :
     (n + 1).ascFactorial k = k ! * (n + k).choose k := by
-  rw [mul_comm]
-  apply mul_right_cancel₀ (factorial_ne_zero (n + k - k))
+  rw [Nat.mul_comm]
+  apply Nat.mul_right_cancel (n + k - k).factorial_pos
   rw [choose_mul_factorial_mul_factorial <| Nat.le_add_left k n, Nat.add_sub_cancel_right,
-    ← factorial_mul_ascFactorial, mul_comm]
+    ← factorial_mul_ascFactorial, Nat.mul_comm]
 #align nat.asc_factorial_eq_factorial_mul_choose Nat.ascFactorial_eq_factorial_mul_choose
 
 theorem ascFactorial_eq_factorial_mul_choose' (n k : ℕ) :
     n.ascFactorial k = k ! * (n + k - 1).choose k := by
   cases n
   · cases k
-    · rw [ascFactorial_zero, choose_zero_right, factorial_zero, mul_one]
-    · simp only [zero_ascFactorial, zero_eq, zero_add, ge_iff_le, succ_sub_succ_eq_sub,
-        Nat.le_zero_eq, Nat.sub_zero, choose_succ_self, mul_zero]
+    · rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]
+    · simp only [zero_ascFactorial, zero_eq, Nat.zero_add, succ_sub_succ_eq_sub,
+        Nat.le_zero_eq, Nat.sub_zero, choose_succ_self, Nat.mul_zero]
   rw [ascFactorial_eq_factorial_mul_choose]
-  simp only [ge_iff_le, succ_add_sub_one]
+  simp only [succ_add_sub_one]
 
 theorem factorial_dvd_ascFactorial (n k : ℕ) : k ! ∣ n.ascFactorial k :=
   ⟨(n + k - 1).choose k, ascFactorial_eq_factorial_mul_choose' _ _⟩
 #align nat.factorial_dvd_asc_factorial Nat.factorial_dvd_ascFactorial
 
 theorem choose_eq_asc_factorial_div_factorial (n k : ℕ) :
     (n + k).choose k = (n + 1).ascFactorial k / k ! := by
-  apply mul_left_cancel₀ (factorial_ne_zero k)
+  apply Nat.mul_left_cancel k.factorial_pos
   rw [← ascFactorial_eq_factorial_mul_choose]
   exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
 #align nat.choose_eq_asc_factorial_div_factorial Nat.choose_eq_asc_factorial_div_factorial
 
 theorem choose_eq_asc_factorial_div_factorial' (n k : ℕ) :
-    (n + k - 1).choose k = n.ascFactorial k / k ! := by
-  apply mul_left_cancel₀ (factorial_ne_zero k)
-  rw [← ascFactorial_eq_factorial_mul_choose']
-  exact (Nat.mul_div_cancel' <| factorial_dvd_ascFactorial _ _).symm
+    (n + k - 1).choose k = n.ascFactorial k / k ! :=
+  Nat.eq_div_of_mul_eq_right k.factorial_ne_zero (ascFactorial_eq_factorial_mul_choose' _ _).symm
 
 theorem descFactorial_eq_factorial_mul_choose (n k : ℕ) : n.descFactorial k = k ! * n.choose k := by
   obtain h | h := Nat.lt_or_ge n k
-  · rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, mul_zero]
-  rw [mul_comm]
-  apply mul_right_cancel₀ (factorial_ne_zero (n - k))
-  rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, mul_comm]
+  · rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, Nat.mul_zero]
+  rw [Nat.mul_comm]
+  apply Nat.mul_right_cancel (n - k).factorial_pos
+  rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, Nat.mul_comm]
 #align nat.desc_factorial_eq_factorial_mul_choose Nat.descFactorial_eq_factorial_mul_choose
 
 theorem factorial_dvd_descFactorial (n k : ℕ) : k ! ∣ n.descFactorial k :=
   ⟨n.choose k, descFactorial_eq_factorial_mul_choose _ _⟩
 #align nat.factorial_dvd_desc_factorial Nat.factorial_dvd_descFactorial
 
-theorem choose_eq_descFactorial_div_factorial (n k : ℕ) : n.choose k = n.descFactorial k / k ! := by
-  apply mul_left_cancel₀ (factorial_ne_zero k)
-  rw [← descFactorial_eq_factorial_mul_choose]
-  exact (Nat.mul_div_cancel' <| factorial_dvd_descFactorial _ _).symm
+theorem choose_eq_descFactorial_div_factorial (n k : ℕ) : n.choose k = n.descFactorial k / k ! :=
+  Nat.eq_div_of_mul_eq_right k.factorial_ne_zero (descFactorial_eq_factorial_mul_choose _ _).symm
 #align nat.choose_eq_desc_factorial_div_factorial Nat.choose_eq_descFactorial_div_factorial
 
 /-- A faster implementation of `choose`, to be used during bytecode evaluation
@@ -302,7 +298,7 @@ theorem choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) :
   refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))
   rw [← choose_succ_right_eq]
   apply Nat.mul_le_mul_left
-  rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← mul_two]
+  rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]
   exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)
 #align nat.choose_le_succ_of_lt_half_left Nat.choose_le_succ_of_lt_half_left
 
@@ -324,7 +320,7 @@ theorem choose_le_middle (r n : ℕ) : choose n r ≤ choose n (n / 2) := by
       apply choose_le_middle_of_le_half_left
       rw [div_lt_iff_lt_mul' Nat.zero_lt_two] at h
       rw [le_div_iff_mul_le' Nat.zero_lt_two, Nat.mul_sub_right_distrib, Nat.sub_le_iff_le_add,
-        ← Nat.sub_le_iff_le_add', mul_two, Nat.add_sub_cancel]
+        ← Nat.sub_le_iff_le_add', Nat.mul_two, Nat.add_sub_cancel]
       exact le_of_lt h
   · rw [choose_eq_zero_of_lt b]
     apply zero_le
@@ -401,7 +397,7 @@ theorem multichoose_one (k : ℕ) : multichoose 1 k = 1 := by
 theorem multichoose_two (k : ℕ) : multichoose 2 k = k + 1 := by
   induction' k with k IH; · simp
   rw [multichoose, IH]
-  simp [add_comm, succ_eq_add_one]
+  simp [Nat.add_comm, succ_eq_add_one]
 #align nat.multichoose_two Nat.multichoose_two
 
 @[simp]
@@ -416,7 +412,8 @@ theorem multichoose_eq : ∀ n k : ℕ, multichoose n k = (n + k - 1).choose k
   | n + 1, k + 1 => by
     have : n + (k + 1) < (n + 1) + (k + 1) := Nat.add_lt_add_right (Nat.lt_succ_self _) _
     have : (n + 1) + k < (n + 1) + (k + 1) := Nat.add_lt_add_left (Nat.lt_succ_self _) _
-    erw [multichoose_succ_succ, add_comm, Nat.succ_add_sub_one, ← add_assoc, Nat.choose_succ_succ]
+    erw [multichoose_succ_succ, Nat.add_comm, Nat.succ_add_sub_one, ← Nat.add_assoc,
+      Nat.choose_succ_succ]
     simp [multichoose_eq n (k+1), multichoose_eq (n+1) k]
   termination_by a b => a + b
   decreasing_by all_goals assumption

Mathlib/Data/Nat/Defs.lean

@@ -636,6 +636,12 @@ lemma div_eq_sub_mod_div : m / n = (m - m % n) / n := by
     rw [this, mul_div_right _ hn]
 #align nat.div_eq_sub_mod_div Nat.div_eq_sub_mod_div
 
+protected lemma eq_div_of_mul_eq_left (hc : c ≠ 0) (h : a * c = b) : a = b / c := by
+  rw [← h, Nat.mul_div_cancel _ (Nat.pos_iff_ne_zero.2 hc)]
+
+protected lemma eq_div_of_mul_eq_right (hc : c ≠ 0) (h : c * a = b) : a = b / c := by
+  rw [← h, Nat.mul_div_cancel_left _ (Nat.pos_iff_ne_zero.2 hc)]
+
 /-!
 ### `pow`