chore(*.ModEq): reduce dependencies (#17154)

Both `Nat.ModEq` and `Int.ModEq` have some spurious dependencies which can be removed by reasonable swaps of generic tactics/declarations for `Nat` and `Int` native versions (e.g. use `omega` more). This PR does that and makes a slouching attempt to hold back the import graph downstream of these.



Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>

Author: mattrobball

Mathlib/Algebra/CharP/Defs.lean

@@ -11,6 +11,7 @@ import Mathlib.Data.Nat.Cast.Prod
 import Mathlib.Data.Nat.Find
 import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.Data.ULift
+import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # Characteristic of semirings
@@ -102,10 +103,10 @@ lemma intCast_injOn_Ico [IsRightCancelAdd R] : InjOn (Int.cast : ℤ → R) (Ico
 
 lemma intCast_eq_zero_iff (a : ℤ) : (a : R) = 0 ↔ (p : ℤ) ∣ a := by
   rcases lt_trichotomy a 0 with (h | rfl | h)
-  · rw [← neg_eq_zero, ← Int.cast_neg, ← dvd_neg]
+  · rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
     lift -a to ℕ using neg_nonneg.mpr (le_of_lt h) with b
     rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
-  · simp only [Int.cast_zero, eq_self_iff_true, dvd_zero]
+  · simp only [Int.cast_zero, eq_self_iff_true, Int.dvd_zero]
   · lift a to ℕ using le_of_lt h with b
     rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]
 

Mathlib/Algebra/ModEq.lean

@@ -5,6 +5,7 @@ Authors: Yaël Dillies
 -/
 import Mathlib.Data.Int.ModEq
 import Mathlib.Algebra.Field.Basic
+import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.GroupTheory.QuotientGroup.Basic
 
 /-!

Mathlib/Algebra/Order/Group/Unbundled/Int.lean

@@ -82,6 +82,15 @@ theorem abs_le_one_iff {a : ℤ} : |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1 := b
 theorem one_le_abs {z : ℤ} (h₀ : z ≠ 0) : 1 ≤ |z| :=
   add_one_le_iff.mpr (abs_pos.mpr h₀)
 
+lemma eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) : x = 0 := by
+  by_contra h
+  have := Int.natAbs_le_of_dvd_ne_zero h1 h
+  rw [Int.abs_eq_natAbs] at h2
+  omega
+
+lemma abs_sub_lt_of_lt_lt {m a b : ℕ} (ha : a < m) (hb : b < m) : |(b : ℤ) - a| < m := by
+  rw [abs_lt]; omega
+
 /-! #### `/`  -/
 
 theorem ediv_eq_zero_of_lt_abs {a b : ℤ} (H1 : 0 ≤ a) (H2 : a < |b|) : a / b = 0 :=

Mathlib/Combinatorics/Additive/FreimanHom.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.CharP.Defs
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.Order.BigOperators.Group.Multiset
+import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.ZMod.Defs
 
 /-!

Mathlib/Data/Int/ModEq.lean

@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Tactic.Abel
-import Mathlib.Tactic.GCongr.CoreAttrs
 
 /-!
 
@@ -92,8 +90,7 @@ theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
 
 @[simp]
 theorem neg_modEq_neg : -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
--- Porting note: Restore old proof once #3309 is through
-  simp [-sub_neg_eq_add, neg_sub_neg, modEq_iff_dvd, dvd_sub_comm]
+  simp only [modEq_iff_dvd, (by omega : -b - -a = -(b - a)), Int.dvd_neg]
 
 @[simp]
 theorem modEq_neg : a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] := by simp [modEq_iff_dvd]
@@ -105,17 +102,17 @@ protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m]
 
 protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] := by
   obtain hc | rfl | hc := lt_trichotomy c 0
-  · rw [← neg_modEq_neg, ← modEq_neg, ← neg_mul, ← neg_mul, ← neg_mul]
+  · rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]
     simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
-  · simp only [zero_mul, ModEq.rfl]
+  · simp only [Int.zero_mul, ModEq.rfl]
   · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]
 
 protected theorem mul_right' (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c] := by
   rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left'
 
 @[gcongr]
 protected theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
-  modEq_iff_dvd.2 <| by convert dvd_add h₁.dvd h₂.dvd using 1; abel
+  modEq_iff_dvd.2 <| by convert Int.dvd_add h₁.dvd h₂.dvd using 1; omega
 
 @[gcongr] protected theorem add_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c + a ≡ c + b [ZMOD n] :=
   ModEq.rfl.add h
@@ -125,10 +122,10 @@ protected theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a +
 
 protected theorem add_left_cancel (h₁ : a ≡ b [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) :
     c ≡ d [ZMOD n] :=
-  have : d - c = b + d - (a + c) - (b - a) := by abel
+  have : d - c = b + d - (a + c) - (b - a) := by omega
   modEq_iff_dvd.2 <| by
     rw [this]
-    exact dvd_sub h₂.dvd h₁.dvd
+    exact Int.dvd_sub h₂.dvd h₁.dvd
 
 protected theorem add_left_cancel' (c : ℤ) (h : c + a ≡ c + b [ZMOD n]) : a ≡ b [ZMOD n] :=
   ModEq.rfl.add_left_cancel h
@@ -183,7 +180,7 @@ theorem cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) :
   rw [modEq_iff_dvd] at h ⊢
   -- Porting note: removed `show` due to leanprover-community/mathlib4#3305
   refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
-  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) gcd_dvd_right, sub_mul]
+  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) gcd_dvd_right, Int.sub_mul]
     exact Int.ediv_dvd_ediv gcd_dvd_left h
   · rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_ofNat,
       Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]
@@ -233,7 +230,7 @@ theorem modEq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n *
     _ ≡ b [ZMOD n] := by rw [add_zero]
 
 theorem modEq_sub_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n] := by
-  convert Int.modEq_add_fac (-c) ha using 1; rw [mul_neg, sub_eq_add_neg]
+  convert Int.modEq_add_fac (-c) ha using 1; rw [Int.mul_neg, sub_eq_add_neg]
 
 theorem modEq_add_fac_self {a t n : ℤ} : a + n * t ≡ a [ZMOD n] :=
   modEq_add_fac _ ModEq.rfl

Mathlib/Data/Int/Order/Lemmas.lean

@@ -34,15 +34,4 @@ theorem natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a
   rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
   exact Int.ofNat_le.symm
 
-/-! ### units -/
-
-
-theorem eq_zero_of_abs_lt_dvd {m x : ℤ} (h1 : m ∣ x) (h2 : |x| < m) : x = 0 := by
-  obtain rfl | hm := eq_or_ne m 0
-  · exact Int.zero_dvd.1 h1
-  rcases h1 with ⟨d, rfl⟩
-  apply mul_eq_zero_of_right
-  rw [← abs_lt_one_iff, ← mul_lt_iff_lt_one_right (abs_pos.mpr hm), ← abs_mul]
-  exact lt_of_lt_of_le h2 (le_abs_self m)
-
 end Int

Mathlib/Data/Nat/ModEq.lean

@@ -3,10 +3,8 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Ring.Regular
+import Mathlib.Algebra.Order.Group.Unbundled.Int
 import Mathlib.Data.Int.GCD
-import Mathlib.Data.Int.Order.Lemmas
-import Mathlib.Tactic.NormNum.Basic
 
 /-!
 # Congruences modulo a natural number
@@ -24,6 +22,7 @@ and proves basic properties about it such as the Chinese Remainder Theorem
 ModEq, congruence, mod, MOD, modulo
 -/
 
+assert_not_exists OrderedAddCommMonoid
 assert_not_exists Function.support
 
 namespace Nat
@@ -37,8 +36,8 @@ notation:50 a " ≡ " b " [MOD " n "]" => ModEq n a b
 
 variable {m n a b c d : ℕ}
 
--- Porting note: This instance should be derivable automatically
-instance : Decidable (ModEq n a b) := decEq (a % n) (b % n)
+-- Since `ModEq` is semi-reducible, we need to provide the decidable instance manually
+instance : Decidable (ModEq n a b) := inferInstanceAs <| Decidable (a % n = b % n)
 
 namespace ModEq
 
@@ -91,7 +90,7 @@ theorem mod_modEq (a n) : a % n ≡ a [MOD n] :=
 namespace ModEq
 
 lemma of_dvd (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m] :=
-  modEq_of_dvd <| d.natCast.trans h.dvd
+  modEq_of_dvd <| Int.ofNat_dvd.mpr d |>.trans h.dvd
 
 protected theorem mul_left' (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD c * n] := by
   unfold ModEq at *; rw [mul_mod_mul_left, mul_mod_mul_left, h]
@@ -122,7 +121,7 @@ protected theorem pow (m : ℕ) (h : a ≡ b [MOD n]) : a ^ m ≡ b ^ m [MOD n]
 @[gcongr]
 protected theorem add (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n] := by
   rw [modEq_iff_dvd, Int.ofNat_add, Int.ofNat_add, add_sub_add_comm]
-  exact dvd_add h₁.dvd h₂.dvd
+  exact Int.dvd_add h₁.dvd h₂.dvd
 
 @[gcongr]
 protected theorem add_left (c : ℕ) (h : a ≡ b [MOD n]) : c + a ≡ c + b [MOD n] :=
@@ -136,7 +135,7 @@ protected theorem add_left_cancel (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b +
     c ≡ d [MOD n] := by
   simp only [modEq_iff_dvd, Int.ofNat_add] at *
   rw [add_sub_add_comm] at h₂
-  convert _root_.dvd_sub h₂ h₁ using 1
+  convert Int.dvd_sub h₂ h₁ using 1
   rw [add_sub_cancel_left]
 
 protected theorem add_left_cancel' (c : ℕ) (h : c + a ≡ c + b [MOD n]) : a ≡ b [MOD n] :=
@@ -155,7 +154,8 @@ protected theorem add_right_cancel' (c : ℕ) (h : a + c ≡ b + c [MOD n]) : a
 For cancelling left multiplication in the modulus, see `Nat.ModEq.of_mul_left`. -/
 protected theorem mul_left_cancel' {a b c m : ℕ} (hc : c ≠ 0) :
     c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m] := by
-  simp [modEq_iff_dvd, ← mul_sub, mul_dvd_mul_iff_left (by simp [hc] : (c : ℤ) ≠ 0)]
+  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]
+  exact fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)
 
 protected theorem mul_left_cancel_iff' {a b c m : ℕ} (hc : c ≠ 0) :
     c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m] :=
@@ -166,7 +166,8 @@ protected theorem mul_left_cancel_iff' {a b c m : ℕ} (hc : c ≠ 0) :
 For cancelling right multiplication in the modulus, see `Nat.ModEq.of_mul_right`. -/
 protected theorem mul_right_cancel' {a b c m : ℕ} (hc : c ≠ 0) :
     a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m] := by
-  simp [modEq_iff_dvd, ← sub_mul, mul_dvd_mul_iff_right (by simp [hc] : (c : ℤ) ≠ 0)]
+  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
+  exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)
 
 protected theorem mul_right_cancel_iff' {a b c m : ℕ} (hc : c ≠ 0) :
     a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m] :=
@@ -204,10 +205,10 @@ namespace ModEq
 theorem le_of_lt_add (h1 : a ≡ b [MOD m]) (h2 : a < b + m) : a ≤ b :=
   (le_total a b).elim id fun h3 =>
     Nat.le_of_sub_eq_zero
-      (eq_zero_of_dvd_of_lt ((modEq_iff_dvd' h3).mp h1.symm) ((tsub_lt_iff_left h3).mpr h2))
+      (eq_zero_of_dvd_of_lt ((modEq_iff_dvd' h3).mp h1.symm) (by omega))
 
 theorem add_le_of_lt (h1 : a ≡ b [MOD m]) (h2 : a < b) : a + m ≤ b :=
-  le_of_lt_add (add_modEq_right.trans h1) (add_lt_add_right h2 m)
+  le_of_lt_add (add_modEq_right.trans h1) (by omega)
 
 theorem dvd_iff (h : a ≡ b [MOD m]) (hdm : d ∣ m) : d ∣ a ↔ d ∣ b := by
   simp only [← modEq_zero_iff_dvd]
@@ -227,9 +228,7 @@ lemma eq_of_abs_lt (h : a ≡ b [MOD m]) (h2 : |(b : ℤ) - a| < m) : a = b := b
   exact Int.eq_zero_of_abs_lt_dvd h.dvd h2
 
 lemma eq_of_lt_of_lt (h : a ≡ b [MOD m]) (ha : a < m) (hb : b < m) : a = b :=
-  h.eq_of_abs_lt <| abs_sub_lt_iff.2
-    ⟨(sub_le_self _ <| Int.natCast_nonneg _).trans_lt <| Int.ofNat_lt.2 hb,
-    (sub_le_self _ <| Int.natCast_nonneg _).trans_lt <| Int.ofNat_lt.2 ha⟩
+  h.eq_of_abs_lt <| Int.abs_sub_lt_of_lt_lt ha hb
 
 /-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c` -/
 lemma cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) :  a ≡ b [MOD m / gcd m c] := by
@@ -241,7 +240,7 @@ lemma cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) :  a ≡ b
   · show (m / d : ℤ) ∣ c / d * (b - a)
     rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
     apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
-    rw [mul_sub]
+    rw [Int.mul_sub]
     exact modEq_iff_dvd.mp h
   · show Int.gcd (m / d) (c / d) = 1
     simp only [← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d), gcd_div hmd hcd,
@@ -299,18 +298,18 @@ def chineseRemainder' (h : a ≡ b [MOD gcd n m]) : { k // k ≡ a [MOD n] ∧ k
         have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
         have := gcd_eq_gcd_ab n m
         constructor <;> rw [Int.emod_def, ← sub_add] <;>
-            refine dvd_add ?_ (dvd_mul_of_dvd_left ?_ _) <;>
+            refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _) <;>
           try norm_cast
         · rw [← sub_eq_iff_eq_add'] at this
-          rw [← this, sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← mul_sub,
+          rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub,
             Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left _ hnonzero,
-            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, dvd_neg, mul_assoc]
+            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg, mul_assoc]
           · exact dvd_mul_right _ _
           norm_cast
           exact dvd_mul_right _ _
         · exact dvd_lcm_left n m
         · rw [← sub_eq_iff_eq_add] at this
-          rw [← this, sub_mul, sub_add, ← mul_sub, Int.sub_ediv_of_dvd,
+          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
             Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
             zero_add, mul_assoc]
           · exact dvd_mul_right _ _
@@ -407,7 +406,7 @@ protected theorem add_div_of_dvd_right {a b c : ℕ} (hca : c ∣ a) : (a + b) /
     add_div_eq_of_add_mod_lt
       (by
         rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
-        exact Nat.mod_lt _ (pos_iff_ne_zero.mpr h))
+        exact Nat.mod_lt _ (zero_lt_of_ne_zero h))
 
 protected theorem add_div_of_dvd_left {a b c : ℕ} (hca : c ∣ b) : (a + b) / c = a / c + b / c := by
   rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]
@@ -430,27 +429,24 @@ theorem odd_mul_odd {n m : ℕ} : n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1 := b
 
 theorem odd_mul_odd_div_two {m n : ℕ} (hm1 : m % 2 = 1) (hn1 : n % 2 = 1) :
     m * n / 2 = m * (n / 2) + m / 2 :=
-  have hm0 : 0 < m := Nat.pos_of_ne_zero fun h => by simp_all
   have hn0 : 0 < n := Nat.pos_of_ne_zero fun h => by simp_all
   mul_right_injective₀ two_ne_zero <| by
     dsimp
     rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
-      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), mul_tsub, mul_one, ←
-      add_tsub_assoc_of_le (succ_le_of_lt hm0),
-      tsub_add_cancel_of_le (le_mul_of_one_le_right (Nat.zero_le _) hn0)]
+      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
+      Nat.add_sub_assoc (by omega), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]
 
 theorem odd_of_mod_four_eq_one {n : ℕ} : n % 4 = 1 → n % 2 = 1 := by
-  simpa [ModEq, show 2 * 2 = 4 by norm_num] using @ModEq.of_mul_left 2 n 1 2
+  simpa [ModEq] using @ModEq.of_mul_left 2 n 1 2
 
 theorem odd_of_mod_four_eq_three {n : ℕ} : n % 4 = 3 → n % 2 = 1 := by
-  simpa [ModEq, show 2 * 2 = 4 by norm_num, show 3 % 4 = 3 by norm_num] using
-    @ModEq.of_mul_left 2 n 3 2
+  simpa [ModEq] using @ModEq.of_mul_left 2 n 3 2
 
 /-- A natural number is odd iff it has residue `1` or `3` mod `4`-/
 theorem odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
   have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := by decide
   ⟨fun hn =>
-    help (n % 4) (mod_lt n (by norm_num)) <| (mod_mod_of_dvd n (by decide : 2 ∣ 4)).trans hn,
+    help (n % 4) (mod_lt n (by omega)) <| (mod_mod_of_dvd n (by decide : 2 ∣ 4)).trans hn,
     fun h => Or.elim h odd_of_mod_four_eq_one odd_of_mod_four_eq_three⟩
 
 lemma mod_eq_of_modEq {a b n} (h : a ≡ b [MOD n]) (hb : b < n) : a % n = b :=

Mathlib/Data/ZMod/Defs.lean

@@ -5,6 +5,7 @@ Authors: Eric Rodriguez
 -/
 import Mathlib.Algebra.Group.Fin.Basic
 import Mathlib.Algebra.NeZero
+import Mathlib.Algebra.Ring.Int
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Fintype.Card
 

Mathlib/Logic/Godel/GodelBetaFunction.lean

@@ -76,8 +76,7 @@ private lemma pairwise_coprime_coprimes (a : Fin m → ℕ) : Pairwise (Coprime
   have hja : j < supOfSeq a := lt_of_lt_of_le j.prop (le_step (le_max_left _ _))
   exact coprime_mul_succ
     (Nat.succ_le_succ <| le_of_lt ltij)
-    (Nat.dvd_factorial
-      (by simp [Nat.succ_sub_succ, ltij])
+    (Nat.dvd_factorial (by omega)
       (by simpa only [Nat.succ_sub_succ] using le_of_lt (lt_of_le_of_lt (sub_le j i) hja)))
 
 /-- Gödel's Beta Function. This is similar to `(Encodable.decodeList).get i`, but it is easier to

Mathlib/Order/Filter/AtTopBot/ModEq.lean

@@ -3,7 +3,10 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Mathlib.Algebra.Order.Ring.Abs
+import Mathlib.Algebra.Order.Ring.Basic
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Algebra.Ring.Divisibility.Basic
+import Mathlib.Algebra.Ring.Int
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Order.Filter.AtTopBot.Monoid