chore: upstream nat compare lemmas

src/Init/Data/Nat.lean

@@ -17,3 +17,5 @@ import Init.Data.Nat.Linear
 import Init.Data.Nat.SOM
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
+import Init.Data.Nat.Lcm
+import Init.Data.Nat.Compare

src/Init/Data/Nat/Compare.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
+prelude
+import Init.Classical
+import Init.Data.Ord
+
+/-! # Basic lemmas about comparing natural numbers
+
+This file introduce some basic lemmas about compare as applied to natural
+numbers.
+-/
+namespace Nat
+
+theorem compare_def_lt (a b : Nat) :
+    compare a b = if a < b then .lt else if b < a then .gt else .eq := by
+  simp only [compare, compareOfLessAndEq]
+  split
+  · rfl
+  · next h =>
+    match Nat.lt_or_eq_of_le (Nat.not_lt.1 h) with
+    | .inl h => simp [h, Nat.ne_of_gt h]
+    | .inr rfl => simp
+
+theorem compare_def_le (a b : Nat) :
+    compare a b = if a ≤ b then if b ≤ a then .eq else .lt else .gt := by
+  rw [compare_def_lt]
+  split
+  · next hlt => simp [Nat.le_of_lt hlt, Nat.not_le.2 hlt]
+  · next hge =>
+    split
+    · next hgt => simp [Nat.le_of_lt hgt, Nat.not_le.2 hgt]
+    · next hle => simp [Nat.not_lt.1 hge, Nat.not_lt.1 hle]
+
+protected theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a := by
+  simp only [compare_def_le]; (repeat' split) <;> try rfl
+  next h1 h2 => cases h1 (Nat.le_of_not_le h2)
+
+protected theorem compare_eq_eq {a b : Nat} : compare a b = .eq ↔ a = b := by
+  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.ne_of_lt, Nat.ne_of_gt, *]
+  next hlt hgt => exact Nat.le_antisymm (Nat.not_lt.1 hgt) (Nat.not_lt.1 hlt)
+
+protected theorem compare_eq_lt {a b : Nat} : compare a b = .lt ↔ a < b := by
+  rw [compare_def_lt]; (repeat' split) <;> simp [*]
+
+protected theorem compare_eq_gt {a b : Nat} : compare a b = .gt ↔ b < a := by
+  rw [compare_def_lt]; (repeat' split) <;> simp [Nat.le_of_lt, *]
+
+protected theorem compare_ne_gt {a b : Nat} : compare a b ≠ .gt ↔ a ≤ b := by
+  rw [compare_def_le]; (repeat' split) <;> simp [*]
+
+protected theorem compare_ne_lt {a b : Nat} : compare a b ≠ .lt ↔ b ≤ a := by
+  rw [compare_def_le]; (repeat' split) <;> simp [Nat.le_of_not_le, *]
+
+end Nat

src/Init/Data/Nat/Div.lean

@@ -327,4 +327,50 @@ theorem div_eq_of_lt (h₀ : a < b) : a / b = 0 := by
   intro h₁
   apply Nat.not_le_of_gt h₀ h₁.right
 
+protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
+  let t := add_mul_div_right 0 m H
+  rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
+
+protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m := by
+  rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
+
+protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
+  | 0, _ => by simp [Nat.div_zero, n.zero_le]
+  | succ k, h => by
+    suffices succ k * (m / succ k) ≤ succ k * n from
+      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
+    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
+    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
+    have h3 : m ≤ succ k * n := h
+    rw [← h2] at h3
+    exact Nat.le_trans h1 h3
+
+@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
+  induction n <;> simp_all [mul_succ]
+
+@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
+  rw [Nat.mul_comm, mul_div_right _ H]
+
+protected theorem div_self (H : 0 < n) : n / n = 1 := by
+  let t := add_div_right 0 H
+  rwa [Nat.zero_add, Nat.zero_div] at t
+
+protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
+by rw [H2, Nat.mul_div_cancel _ H1]
+
+protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
+by rw [H2, Nat.mul_div_cancel_left _ H1]
+
+protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
+    m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
+
+protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
+    n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]
+
+theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
+  match n, Nat.eq_zero_or_pos n with
+  | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
+  | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
+
+
 end Nat

src/Init/Data/Nat/Dvd.lean

@@ -104,4 +104,36 @@ protected theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m := by
   subst h
   rw [Nat.mul_assoc, add_mul_mod_self_left]
 
+protected theorem dvd_of_mul_dvd_mul_left
+    (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n := by
+  let ⟨l, H⟩ := H
+  rw [Nat.mul_assoc] at H
+  exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩
+
+protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
+  rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
+
+theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
+  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
+
+protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
+  | ⟨e, he⟩, ⟨f, hf⟩ =>
+    ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩
+
+protected theorem mul_dvd_mul_left (a : Nat) (h : b ∣ c) : a * b ∣ a * c :=
+  Nat.mul_dvd_mul (Nat.dvd_refl a) h
+
+protected theorem mul_dvd_mul_right (h: a ∣ b) (c : Nat) : a * c ∣ b * c :=
+  Nat.mul_dvd_mul h (Nat.dvd_refl c)
+
+@[simp] theorem dvd_one {n : Nat} : n ∣ 1 ↔ n = 1 :=
+  ⟨eq_one_of_dvd_one, fun h => h.symm ▸ Nat.dvd_refl _⟩
+
+protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k) := by
+  match Nat.eq_zero_or_pos k with
+  | .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
+  | .inr hpos =>
+    have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
+    rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
+
 end Nat

src/Init/Data/Nat/Gcd.lean

@@ -1,10 +1,12 @@
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Dvd
+import Init.NotationExtra
+import Init.RCases
 
 namespace Nat
 
@@ -14,8 +16,8 @@ def gcd (m n : @& Nat) : Nat :=
     n
   else
     gcd (n % m) m
-termination_by m
-decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
+  termination_by m
+  decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption
 
 @[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y :=
   rfl
@@ -69,4 +71,166 @@ theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
   | H0 n => rw [gcd_zero_left]; exact kn
   | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km
 
+theorem dvd_gcd_iff : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n :=
+  ⟨fun h => let ⟨h₁, h₂⟩ := gcd_dvd m n; ⟨Nat.dvd_trans h h₁, Nat.dvd_trans h h₂⟩,
+   fun ⟨h₁, h₂⟩ => dvd_gcd h₁ h₂⟩
+
+theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
+  Nat.dvd_antisymm
+    (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
+    (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))
+
+theorem gcd_eq_left_iff_dvd : m ∣ n ↔ gcd m n = m :=
+  ⟨fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left],
+   fun h => h ▸ gcd_dvd_right m n⟩
+
+theorem gcd_eq_right_iff_dvd : m ∣ n ↔ gcd n m = m := by
+  rw [gcd_comm]; exact gcd_eq_left_iff_dvd
+
+theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
+  Nat.dvd_antisymm
+    (dvd_gcd
+      (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
+      (dvd_gcd (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
+        (gcd_dvd_right (gcd m n) k)))
+    (dvd_gcd
+      (dvd_gcd (gcd_dvd_left m (gcd n k))
+        (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
+      (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
+
+@[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)
+
+theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by
+  induction n, k using gcd.induction with
+  | H0 k => simp
+  | H1 n k _ IH => rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH
+
+theorem gcd_mul_right (m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n := by
+  rw [Nat.mul_comm m n, Nat.mul_comm k n, Nat.mul_comm (gcd m k) n, gcd_mul_left]
+
+theorem gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) : 0 < gcd m n :=
+  pos_of_dvd_of_pos (gcd_dvd_left m n) mpos
+
+theorem gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) : 0 < gcd m n :=
+  pos_of_dvd_of_pos (gcd_dvd_right m n) npos
+
+theorem div_gcd_pos_of_pos_left (b : Nat) (h : 0 < a) : 0 < a / a.gcd b :=
+  (Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_left _ h).2 (Nat.one_mul _ ▸ Nat.gcd_le_left _ h)
+
+theorem div_gcd_pos_of_pos_right (a : Nat) (h : 0 < b) : 0 < b / a.gcd b :=
+  (Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_right _ h).2 (Nat.one_mul _ ▸ Nat.gcd_le_right _ h)
+
+theorem eq_zero_of_gcd_eq_zero_left {m n : Nat} (H : gcd m n = 0) : m = 0 :=
+  match eq_zero_or_pos m with
+  | .inl H0 => H0
+  | .inr H1 => absurd (Eq.symm H) (ne_of_lt (gcd_pos_of_pos_left _ H1))
+
+theorem eq_zero_of_gcd_eq_zero_right {m n : Nat} (H : gcd m n = 0) : n = 0 := by
+  rw [gcd_comm] at H
+  exact eq_zero_of_gcd_eq_zero_left H
+
+theorem gcd_ne_zero_left : m ≠ 0 → gcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_left
+
+theorem gcd_ne_zero_right : n ≠ 0 → gcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_right
+
+theorem gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) :
+    gcd (m / k) (n / k) = gcd m n / k :=
+  match eq_zero_or_pos k with
+  | .inl H0 => by simp [H0]
+  | .inr H3 => by
+    apply Nat.eq_of_mul_eq_mul_right H3
+    rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
+        Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]
+
+theorem gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m ∣ k) : gcd m n ∣ gcd k n :=
+  dvd_gcd (Nat.dvd_trans (gcd_dvd_left m n) H) (gcd_dvd_right m n)
+
+theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m ∣ k) : gcd n m ∣ gcd n k :=
+  dvd_gcd (gcd_dvd_left n m) (Nat.dvd_trans (gcd_dvd_right n m) H)
+
+theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcd m n ∣ gcd (k * m) n :=
+  gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)
+
+theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcd m n ∣ gcd (m * k) n :=
+  gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)
+
+theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcd m n ∣ gcd m (k * n) :=
+  gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)
+
+theorem gcd_dvd_gcd_mul_right_right (m n k : Nat) : gcd m n ∣ gcd m (n * k) :=
+  gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_right _ _)
+
+theorem gcd_eq_left {m n : Nat} (H : m ∣ n) : gcd m n = m :=
+  Nat.dvd_antisymm (gcd_dvd_left _ _) (dvd_gcd (Nat.dvd_refl _) H)
+
+theorem gcd_eq_right {m n : Nat} (H : n ∣ m) : gcd m n = n := by
+  rw [gcd_comm, gcd_eq_left H]
+
+@[simp] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
+  Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (Nat.dvd_mul_left _ _) (Nat.dvd_refl _))
+
+@[simp] theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n := by
+  rw [gcd_comm, gcd_mul_left_left]
+
+@[simp] theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n := by
+  rw [Nat.mul_comm, gcd_mul_left_left]
+
+@[simp] theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n := by
+  rw [gcd_comm, gcd_mul_right_left]
+
+@[simp] theorem gcd_gcd_self_right_left (m n : Nat) : gcd m (gcd m n) = gcd m n :=
+  Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (gcd_dvd_left _ _) (Nat.dvd_refl _))
+
+@[simp] theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m := by
+  rw [gcd_comm n m, gcd_gcd_self_right_left]
+
+@[simp] theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m := by
+  rw [gcd_comm, gcd_gcd_self_right_right]
+
+@[simp] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
+  rw [gcd_comm m n, gcd_gcd_self_left_right]
+
+theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
+  simp [gcd_rec m (n + k * m), gcd_rec m n]
+
+theorem gcd_eq_zero_iff {i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
+  ⟨fun h => ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩,
+   fun h => by simp [h]⟩
+
+/-- Characterization of the value of `Nat.gcd`. -/
+theorem gcd_eq_iff (a b : Nat) :
+    gcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ (∀ c, c ∣ a → c ∣ b → c ∣ g) := by
+  constructor
+  · rintro rfl
+    exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _, fun _ => Nat.dvd_gcd⟩
+  · rintro ⟨ha, hb, hc⟩
+    apply Nat.dvd_antisymm
+    · apply hc
+      · exact gcd_dvd_left a b
+      · exact gcd_dvd_right a b
+    · exact Nat.dvd_gcd ha hb
+
+/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
+def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
+    {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=
+  if h0 : gcd k m = 0 then
+    ⟨⟨⟨0, eq_zero_of_gcd_eq_zero_right h0 ▸ Nat.dvd_refl 0⟩,
+      ⟨n, Nat.dvd_refl n⟩⟩,
+      eq_zero_of_gcd_eq_zero_left h0 ▸ (Nat.zero_mul n).symm⟩
+  else by
+    have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
+    refine ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, ?_⟩⟩, hd.symm⟩
+    apply Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_ne_zero h0)
+    rw [hd, ← gcd_mul_right]
+    exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) H
+
+theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n := by
+  let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
+    prod_dvd_and_dvd_of_dvd_prod <| gcd_dvd_right k (m * n)
+  rw [h]
+  have h' : m' * n' ∣ k := h ▸ gcd_dvd_left ..
+  exact Nat.mul_dvd_mul
+    (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
+    (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')
+
 end Nat

src/Init/Data/Nat/Lcm.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro
+-/
+prelude
+import Init.Data.Nat.Gcd
+import Init.Data.Nat.Lemmas
+
+namespace Nat
+
+/-- The least common multiple of `m` and `n`, defined using `gcd`. -/
+def lcm (m n : Nat) : Nat := m * n / gcd m n
+
+theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
+  rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]
+
+@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]
+
+@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm]
+
+@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]
+
+@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]
+
+@[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
+  match eq_zero_or_pos m with
+  | .inl h => rw [h, lcm_zero_left]
+  | .inr h => simp [lcm, Nat.mul_div_cancel _ h]
+
+theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
+  ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩
+
+theorem dvd_lcm_right (m n : Nat) : n ∣ lcm m n := lcm_comm n m ▸ dvd_lcm_left n m
+
+theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
+  rw [lcm, Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]
+
+theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k := by
+  match eq_zero_or_pos k with
+  | .inl h => rw [h]; exact Nat.dvd_zero _
+  | .inr kpos =>
+    apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
+    rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
+    exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)
+
+theorem lcm_assoc (m n k : Nat) : lcm (lcm m n) k = lcm m (lcm n k) :=
+Nat.dvd_antisymm
+  (lcm_dvd
+    (lcm_dvd (dvd_lcm_left m (lcm n k))
+      (Nat.dvd_trans (dvd_lcm_left n k) (dvd_lcm_right m (lcm n k))))
+    (Nat.dvd_trans (dvd_lcm_right n k) (dvd_lcm_right m (lcm n k))))
+  (lcm_dvd
+    (Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
+    (lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
+      (dvd_lcm_right (lcm m n) k)))
+
+theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 := by
+  intro h
+  have h1 := gcd_mul_lcm m n
+  rw [h, Nat.mul_zero] at h1
+  match mul_eq_zero.1 h1.symm with
+  | .inl hm1 => exact hm hm1
+  | .inr hn1 => exact hn hn1
+
+end Nat

src/Init/Data/Nat/Lemmas.lean

@@ -8,6 +8,7 @@ import Init.Data.Nat.Dvd
 import Init.Data.Nat.MinMax
 import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
+import Init.Omega
 
 /-! # Basic lemmas about natural numbers
 
@@ -335,6 +336,32 @@ protected theorem sub_max_sub_right : ∀ (a b c : Nat), max (a - c) (b - c) = m
   | _, _, 0 => rfl
   | _, _, _+1 => Eq.trans (Nat.pred_max_pred ..) <| congrArg _ (Nat.sub_max_sub_right ..)
 
+protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
+  omega
+
+protected theorem sub_max_sub_left (a b c : Nat) : max (a - b) (a - c) = a - min b c := by
+  omega
+
+protected theorem mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c := by
+  induction a generalizing b with
+  | zero => simp
+  | succ i ind =>
+    cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_max_add_right, ind]
+
+protected theorem mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c := by
+  induction a generalizing b with
+  | zero => simp
+  | succ i ind =>
+    cases b <;> simp [succ_eq_add_one, Nat.succ_mul, Nat.add_min_add_right, ind]
+
+protected theorem mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c := by
+  repeat rw [Nat.mul_comm a]
+  exact Nat.mul_max_mul_right ..
+
+protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c := by
+  repeat rw [Nat.mul_comm a]
+  exact Nat.mul_min_mul_right ..
+
 -- protected theorem sub_min_sub_left (a b c : Nat) : min (a - b) (a - c) = a - max b c := by
 --   induction b, c using Nat.recDiagAux with
 --   | zero_left => rw [Nat.sub_zero, Nat.zero_max]; exact Nat.min_eq_right (Nat.sub_le ..)
@@ -484,51 +511,6 @@ protected theorem pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) : 0 < a := by
 
 /-! ### div/mod -/
 
-protected theorem div_le_of_le_mul {m n : Nat} : ∀ {k}, m ≤ k * n → m / k ≤ n
-  | 0, _ => by simp [Nat.div_zero, n.zero_le]
-  | succ k, h => by
-    suffices succ k * (m / succ k) ≤ succ k * n from
-      Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
-    have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
-    have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
-    have h3 : m ≤ succ k * n := h
-    rw [← h2] at h3
-    exact Nat.le_trans h1 h3
-
-@[simp] theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n := by
-  induction n <;> simp_all [mul_succ]
-
-@[simp] theorem mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
-  rw [Nat.mul_comm, mul_div_right _ H]
-
-protected theorem div_self (H : 0 < n) : n / n = 1 := by
-  let t := add_div_right 0 H
-  rwa [Nat.zero_add, Nat.zero_div] at t
-
-protected theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m := by
-  let t := add_mul_div_right 0 m H
-  rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t
-
-protected theorem mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m :=
-by rw [Nat.mul_comm, Nat.mul_div_cancel _ H]
-
-protected theorem div_eq_of_eq_mul_left (H1 : 0 < n) (H2 : m = k * n) : m / n = k :=
-by rw [H2, Nat.mul_div_cancel _ H1]
-
-protected theorem div_eq_of_eq_mul_right (H1 : 0 < n) (H2 : m = n * k) : m / n = k :=
-by rw [H2, Nat.mul_div_cancel_left _ H1]
-
-protected theorem mul_div_mul_left {m : Nat} (n k : Nat) (H : 0 < m) :
-    m * n / (m * k) = n / k := by rw [← Nat.div_div_eq_div_mul, Nat.mul_div_cancel_left _ H]
-
-protected theorem mul_div_mul_right {m : Nat} (n k : Nat) (H : 0 < m) :
-    n * m / (k * m) = n / k := by rw [Nat.mul_comm, Nat.mul_comm k, Nat.mul_div_mul_left _ _ H]
-
-theorem mul_div_le (m n : Nat) : n * (m / n) ≤ m := by
-  match n, Nat.eq_zero_or_pos n with
-  | _, Or.inl rfl => rw [Nat.zero_mul]; exact m.zero_le
-  | n, Or.inr h => rw [Nat.mul_comm, ← Nat.le_div_iff_mul_le h]; exact Nat.le_refl _
-
 theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
   match n % 2, @Nat.mod_lt n 2 (by decide) with
   | 0, _ => .inl rfl
@@ -719,37 +701,17 @@ theorem lt_log2_self : n < 2 ^ (n.log2 + 1) :=
 
 /-! ### dvd -/
 
-theorem dvd_sub {k m n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n :=
-  (Nat.dvd_add_iff_left h₂).2 <| by rwa [Nat.sub_add_cancel H]
+protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
+    a = b * c := by
+  rw [← H2, Nat.mul_div_cancel' H1]
 
-protected theorem mul_dvd_mul {a b c d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d
-  | ⟨e, he⟩, ⟨f, hf⟩ =>
-    ⟨e * f, by simp [he, hf, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]⟩
+protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
+    a / b = c ↔ a = b * c :=
+  ⟨Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H⟩
 
-protected theorem mul_dvd_mul_left (a : Nat) (h : b ∣ c) : a * b ∣ a * c :=
-  Nat.mul_dvd_mul (Nat.dvd_refl a) h
-
-protected theorem mul_dvd_mul_right (h: a ∣ b) (c : Nat) : a * c ∣ b * c :=
-  Nat.mul_dvd_mul h (Nat.dvd_refl c)
-
-@[simp] theorem dvd_one {n : Nat} : n ∣ 1 ↔ n = 1 :=
-  ⟨eq_one_of_dvd_one, fun h => h.symm ▸ Nat.dvd_refl _⟩
-
-protected theorem mul_div_assoc (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k) := by
-  match Nat.eq_zero_or_pos k with
-  | .inl h0 => rw [h0, Nat.div_zero, Nat.div_zero, Nat.mul_zero]
-  | .inr hpos =>
-    have h1 : m * n / k = m * (n / k * k) / k := by rw [Nat.div_mul_cancel H]
-    rw [h1, ← Nat.mul_assoc, Nat.mul_div_cancel _ hpos]
-
-protected theorem dvd_of_mul_dvd_mul_left
-    (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n := by
-  let ⟨l, H⟩ := H
-  rw [Nat.mul_assoc] at H
-  exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩
-
-protected theorem dvd_of_mul_dvd_mul_right (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n := by
-  rw [Nat.mul_comm m k, Nat.mul_comm n k] at H; exact Nat.dvd_of_mul_dvd_mul_left kpos H
+protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
+    a / b = c ↔ a = c * b := by
+  rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
 
 theorem pow_dvd_pow_iff_pow_le_pow {k l : Nat} :
     ∀ {x : Nat}, 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)
@@ -773,18 +735,6 @@ theorem pow_dvd_pow_iff_le_right {x k l : Nat} (w : 1 < x) : x ^ k ∣ x ^ l ↔
 theorem pow_dvd_pow_iff_le_right' {b k l : Nat} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l :=
   pow_dvd_pow_iff_le_right (Nat.lt_of_sub_eq_succ rfl)
 
-protected theorem eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) :
-    a = b * c := by
-  rw [← H2, Nat.mul_div_cancel' H1]
-
-protected theorem div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
-    a / b = c ↔ a = b * c :=
-  ⟨Nat.eq_mul_of_div_eq_right H', Nat.div_eq_of_eq_mul_right H⟩
-
-protected theorem div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) :
-    a / b = c ↔ a = c * b := by
-  rw [Nat.mul_comm]; exact Nat.div_eq_iff_eq_mul_right H H'
-
 protected theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a ^ n := by
   cases Nat.exists_eq_add_of_le h
   case intro k p =>