awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ HMul.hMul (α := ℤ) (↑c : ℤ) (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) →
    (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
exact fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)

Premises used: Iff.mpr, Int.ofNat_ne_zero, Int.dvd_of_mul_dvd_mul_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m]

Tactic:
⟨ModEq.mul_left_cancel' hc, ModEq.mul_left' _⟩

Premises used: Nat.ModEq.mul_left_cancel', Nat.ModEq.mul_left', Iff.intro
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
simp :
  HMul.hMul (α := ℤ) (↑m : ℤ) (↑c : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) * (↑c : ℤ) →
    (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Tactic:
simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]

Premises used: Int.sub_mul, Nat.modEq_iff_dvd, Int.natCast_mul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ HMul.hMul (α := ℤ) (↑m : ℤ) (↑c : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) * (↑c : ℤ) →
    (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

Premises used: Iff.mpr, Int.ofNat_ne_zero, Int.dvd_of_mul_dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ HMul.hMul (α := ℤ) (↑m : ℤ) (↑c : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) * (↑c : ℤ) →
    (↑m : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

Premises used: Iff.mpr, Int.ofNat_ne_zero, Int.dvd_of_mul_dvd_mul_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c m : ℕ
hc : c ≠ 0
⊢ a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m]

Tactic:
⟨ModEq.mul_right_cancel' hc, ModEq.mul_right' _⟩

Premises used: Iff.intro, Nat.ModEq.mul_right', Nat.ModEq.mul_right_cancel'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b m : ℕ
h : a ≡ b [MOD m * n]
rw : ∀ (h : (↑(m * n) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)), (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD n]

Tactic:
rw [modEq_iff_dvd] at *

Premises used: Nat.modEq_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b m : ℕ
h : (↑(m * n) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
(dvd_mul_left (n : ℤ) (m : ℤ)).trans h

Premises used: Nat.cast, dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b m : ℕ
h : (↑(m * n) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ (↑n : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h

Premises used: Nat.cast, dvd_mul_left, Dvd.dvd.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b m : ℕ
⊢ a ≡ b [MOD n * m] → a ≡ b [MOD n]

Tactic:
mul_comm m n ▸ of_mul_left _

Premises used: Eq.rec, Nat.ModEq.of_mul_left, mul_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
⊢ c * (a / c) ≡ c * (b / c) [MOD c * (m / c)]

Tactic:
h.mul_left' c

Premises used: Nat.ModEq.mul_left'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : m = c * (m / c)
h₂ : a = c * (a / c)
h₃ : b = c * (b / c)
⊢ a ≡ b [MOD m]

Tactic:
convert! h.mul_left' c

Premises used: Nat.ModEq.mul_left'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : m = m
h₂ : c ∣ m
h₃ : m = m
h₄ h₅ h₆ : c ∣ m
⊢ m = c * (m / c)

Tactic:
rwa [Nat.mul_div_cancel']

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : a = a
h₂ : c ∣ a
h₃ : a = a
h₄ h₅ h₆ : c ∣ a
⊢ a = c * (a / c)

Tactic:
rwa [Nat.mul_div_cancel']

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
h : a / c ≡ b / c [MOD m / c]
ha_1 : c ∣ a
ha_2 : c ∣ b
ha : c ∣ m
h₁ : b = b
h₂ : c ∣ b
h₃ : b = b
h₄ h₅ h₆ : c ∣ b
⊢ b = c * (b / c)

Tactic:
rwa [Nat.mul_div_cancel']

Premises used: Nat.mul_div_cancel'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n : ℕ
⊢ n ≡ 0 [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a + b ≡ a [MOD n] ↔ n ∣ b

Tactic:
simp [modEq_iff_dvd, Int.natCast_dvd_natCast]

Premises used: Nat.modEq_iff_dvd, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
rw : b + a ≡ b [MOD n] ↔ n ∣ a
rw₁ rw₂ : n ∣ a ↔ n ∣ a
⊢ a + b ≡ b [MOD n] ↔ n ∣ a

Tactic:
rw [add_comm, add_modEq_left_iff]

Premises used: add_comm, Nat.add_modEq_left_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
rw : a + b ≡ a [MOD n] ↔ n ∣ b
rw₁ rw₂ : n ∣ b ↔ n ∣ b
⊢ a ≡ a + b [MOD n] ↔ n ∣ b

Tactic:
rw [ModEq.comm, add_modEq_left_iff]

Premises used: Nat.add_modEq_left_iff, Nat.ModEq.comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
rw : a + b ≡ b [MOD n] ↔ n ∣ a
rw₁ rw₂ : n ∣ a ↔ n ∣ a
⊢ b ≡ a + b [MOD n] ↔ n ∣ a

Tactic:
rw [ModEq.comm, add_modEq_right_iff]

Premises used: Nat.ModEq.comm, Nat.add_modEq_right_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
rw : a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
rw₁ rw₂ : a ≡ b [MOD n] ↔ a ≡ b [MOD n]
⊢ n + a ≡ b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
rw [add_comm, add_modulus_modEq_iff]

Premises used: Nat.add_modulus_modEq_iff, add_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a ≡ b + n [MOD n] ↔ a ≡ b [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
⊢ a ≡ n + b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
⊢ a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
rw : a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]
rw₁ rw₂ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
⊢ b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
rw [add_comm, add_mul_modulus_modEq_iff]

Premises used: add_comm, Nat.add_mul_modulus_modEq_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
⊢ a ≡ b + c * n [MOD n] ↔ a ≡ b [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
rw : a ≡ c + b * n [MOD n] ↔ a ≡ c [MOD n]
rw₁ rw₂ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
⊢ a ≡ b * n + c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
rw [add_comm, modEq_add_mul_modulus_iff]

Premises used: add_comm, Nat.modEq_add_mul_modulus_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
⊢ a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
rw : a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]
rw₁ rw₂ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
⊢ n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
rw [add_comm, add_modulus_mul_modEq_iff]

Premises used: Nat.add_modulus_mul_modEq_iff, add_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
⊢ a ≡ b + n * c [MOD n] ↔ a ≡ b [MOD n]

Tactic:
simp [ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b c : ℕ
rw : a ≡ c + n * b [MOD n] ↔ a ≡ c [MOD n]
rw₁ rw₂ : a ≡ c [MOD n] ↔ a ≡ c [MOD n]
⊢ a ≡ n * b + c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
rw [add_comm, modEq_add_modulus_mul_iff]

Premises used: add_comm, Nat.modEq_add_modulus_mul_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : n ≤ a
rw : a - n + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
rw₁ rw₂ : a ≡ b [MOD n] ↔ a ≡ b [MOD n]
⊢ a - n ≡ b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
rw [← add_modulus_modEq_iff, Nat.sub_add_cancel h]

Premises used: Nat.add_modulus_modEq_iff, Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : n ≤ b
rw : a ≡ b - n + n [MOD n] ↔ a ≡ b [MOD n]
rw₁ rw₂ : a ≡ b [MOD n] ↔ a ≡ b [MOD n]
⊢ a ≡ b - n [MOD n] ↔ a ≡ b [MOD n]

Tactic:
rw [← modEq_add_modulus_iff, Nat.sub_add_cancel h]

Premises used: Nat.sub_add_cancel, Nat.modEq_add_modulus_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b : ℕ
h : b ≤ a
rw rw₁ : HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ) ∣ HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)
⊢ (↑(a - b) : ℤ) ∣ HSub.hSub (α := ℤ) (↑a : ℤ) (↑b : ℤ)

Tactic:
rw [Int.ofNat_sub h]

Premises used: Int.ofNat_sub
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b : ℕ
⊢ a ≡ b [MOD 1]

Tactic:
modEq_of_dvd <| one_dvd _

Premises used: one_dvd, Nat.modEq_of_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b : ℕ
rw : a % 0 = b % 0 ↔ a = b
rw₁ : a = b % 0 ↔ a = b
rw₂ rw₃ : a = b ↔ a = b
⊢ a ≡ b [MOD 0] ↔ a = b

Tactic:
rw [ModEq, mod_zero, mod_zero]

Premises used: Nat.mod_zero, Nat.ModEq
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
⊢ n + a ≡ a [MOD n]

Tactic:
simp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a : ℕ
⊢ a + n ≡ a [MOD n]

Tactic:
simp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≤ b
rw : (∃ (c : ℕ), b - a = n * c) ↔ ∃ (t : ℕ), b = a + n * t
⊢ a ≡ b [MOD n] ↔ ∃ (t : ℕ), b = a + n * t

Tactic:
rw [modEq_iff_dvd' h, dvd_def]

Premises used: dvd_def, Nat.modEq_iff_dvd'
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≤ b
⊢ (∃ (c : ℕ), b - a = n * c) ↔ ∃ (t : ℕ), b = a + n * t

Tactic:
exists_congr (fun _ => Nat.sub_eq_iff_eq_add' h)

Premises used: Nat.sub_eq_iff_eq_add', exists_congr
-- Module: Mathlib.Data.Nat.ModEq
Goal:
n a b : ℕ
h : a ≤ b
⊢ (∃ (c : ℕ), b - a = n * c) ↔ ∃ (t : ℕ), b = a + n * t

Tactic:
exact exists_congr (fun _ => Nat.sub_eq_iff_eq_add' h)

Premises used: Nat.sub_eq_iff_eq_add', exists_congr
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h1 : a ≡ b [MOD m]
h2 : a < b + m
h3 : b ≤ a
⊢ a - b < m

Tactic:
lia
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h1 : a ≡ b [MOD m]
h2 : a < b
⊢ a + m < b + m

Tactic:
lia
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
simp : a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]
⊢ d ∣ a ↔ d ∣ b

Tactic:
simp only [← modEq_zero_iff_dvd]

Premises used: Nat.modEq_zero_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b d : ℕ
h : a ≡ b [MOD m]
hdm : d ∣ m
⊢ a ≡ b [MOD d]

Tactic:
replace h := h.of_dvd hdm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Tactic:
⟨h.symm.trans, h.trans⟩

Premises used: Nat.ModEq.symm, Iff.intro, Nat.ModEq.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b d : ℕ
hdm : d ∣ m
h : a ≡ b [MOD d]
⊢ a ≡ 0 [MOD d] ↔ b ≡ 0 [MOD d]

Tactic:
exact ⟨h.symm.trans, h.trans⟩
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
⊢ a.gcd m ∣ m

Tactic:
have h1 := gcd_dvd_right a m
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
⊢ b.gcd m ∣ m

Tactic:
have h2 := gcd_dvd_right b m
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
h2 : b.gcd m ∣ m
⊢ a.gcd m = b.gcd m

Tactic:
dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
      (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)

Premises used: Iff.mpr, Nat.gcd_dvd_left, Nat.ModEq.dvd_iff, dvd_antisymm, Nat.dvd_gcd, Iff.mp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h1 : a.gcd m ∣ m
h2 : b.gcd m ∣ m
⊢ a.gcd m = b.gcd m

Tactic:
exact
    dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
      (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)

Premises used: Iff.mpr, Nat.gcd_dvd_left, Nat.ModEq.dvd_iff, dvd_antisymm, Nat.dvd_gcd, Iff.mp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)
x : Int.ofNat a = Int.ofNat b
⊢ a = b

Tactic:
apply Int.ofNat.inj

Premises used: Int.ofNat.inj
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)
x : Int.ofNat b - Int.ofNat a = 0
⊢ Int.ofNat a = Int.ofNat b

Tactic:
rw [eq_comm, ← sub_eq_zero]

Premises used: sub_eq_zero, eq_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)
⊢ Int.ofNat b - Int.ofNat a = 0

Tactic:
Int.eq_zero_of_abs_lt_dvd h.dvd h2

Premises used: Int.eq_zero_of_abs_lt_dvd, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)
⊢ Int.ofNat b - Int.ofNat a = 0

Tactic:
exact Int.eq_zero_of_abs_lt_dvd h.dvd h2

Premises used: Int.eq_zero_of_abs_lt_dvd, Nat.ModEq.dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b : ℕ
h : a ≡ b [MOD m]
ha : a < m
hb : b < m
⊢ a = b

Tactic:
h.eq_of_abs_lt <| Int.abs_sub_lt_of_lt_lt ha hb

Premises used: Int.abs_sub_lt_of_lt_lt, Nat.ModEq.eq_of_abs_lt
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
⊢ m.gcd c ∣ m

Tactic:
have hmd := gcd_dvd_left m c
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
⊢ m.gcd c ∣ c

Tactic:
have hcd := gcd_dvd_right m c
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
rw : (↑(m / m.gcd c) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
rw [modEq_iff_dvd]

Premises used: Nat.modEq_iff_dvd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑(m / m.gcd c) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
@Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_

Premises used: Int.dvd_of_dvd_mul_right_of_gcd_one, Int.ediv
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
refine_1 :
  HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
refine_2 : (HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ)).gcd (HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ)) = 1
⊢ (↑(m / m.gcd c) : ℤ) ∣ HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
refine @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_

Premises used: Int.dvd_of_dvd_mul_right_of_gcd_one
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
refine_1 : HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(m.gcd c) : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]

Premises used: Iff.mpr, Int.mul_ediv_assoc, HSub.hSub, Nat.cast, mul_comm, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
refine_1 : (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ) / (↑(m.gcd c) : ℤ)

Tactic:
apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)

Premises used: Iff.mpr, Int.ediv_dvd_ediv, Int.natCast_dvd_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
refine_1 : (↑m : ℤ) ∣ HMul.hMul (α := ℤ) (↑c : ℤ) (↑b : ℤ) - HMul.hMul (α := ℤ) (↑c : ℤ) (↑a : ℤ)
⊢ (↑m : ℤ) ∣ (↑c : ℤ) * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
rw [Int.mul_sub]

Premises used: Int.mul_sub
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑m : ℤ) ∣ HMul.hMul (α := ℤ) (↑c : ℤ) (↑b : ℤ) - HMul.hMul (α := ℤ) (↑c : ℤ) (↑a : ℤ)

Tactic:
modEq_iff_dvd.mp h

Premises used: Nat.modEq_iff_dvd, Int.mul, Iff.mp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (↑m : ℤ) ∣ HMul.hMul (α := ℤ) (↑c : ℤ) (↑b : ℤ) - HMul.hMul (α := ℤ) (↑c : ℤ) (↑a : ℤ)

Tactic:
exact modEq_iff_dvd.mp h

Premises used: Nat.modEq_iff_dvd, Iff.mp
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : c * a ≡ c * b [MOD m]
d : ℕ := m.gcd c
hmd : m.gcd c ∣ m
hcd : m.gcd c ∣ c
⊢ (HDiv.hDiv (α := ℤ) (↑m : ℤ) (↑d : ℤ)).gcd (HDiv.hDiv (α := ℤ) (↑c : ℤ) (↑d : ℤ)) = 1

Tactic:
simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d),
      gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]

Premises used: HDiv.hDiv, Nat.gcd_pos_of_pos_left, Nat.gcd_div, Int.natCast_div, Nat.div_self, Int.gcd_natCast_natCast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
apply : c * a ≡ c * b [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
apply cancel_left_div_gcd hm

Premises used: Nat.ModEq.cancel_left_div_gcd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
simpa [mul_comm] using h

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c d : ℕ
hm : 0 < m
hcd : c ≡ d [MOD m]
h : c * a ≡ d * b [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
(h.trans <| hcd.symm.mul_right b).cancel_left_div_gcd hm

Premises used: Nat.ModEq.mul_right, Nat.ModEq.symm, Nat.ModEq.cancel_left_div_gcd, Nat.ModEq.trans
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c d : ℕ
hm : 0 < m
hcd : c ≡ d [MOD m]
h : a * c ≡ b * d [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
(h.trans <| hcd.symm.mul_left b).cancel_right_div_gcd hm

Premises used: Nat.ModEq.mul_left, Nat.ModEq.symm, Nat.ModEq.trans, Nat.ModEq.cancel_right_div_gcd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
inl : ∀ (hmc : gcd 0 c = 1) (h : c * a ≡ c * b [MOD 0]), a ≡ b [MOD 0]
inr : ∀ (hm : m > 0), a ≡ b [MOD m]
⊢ a ≡ b [MOD m]

Tactic:
rcases m.eq_zero_or_pos with (rfl | hm)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hmc : gcd 0 c = 1
h : c * a ≡ c * b [MOD 0]
⊢ c = 1

Tactic:
simp only [gcd_zero_left] at hmc

Premises used: Nat.gcd_zero_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
h : c * a ≡ c * b [MOD 0]
hmc : c = 1
⊢ a = b

Tactic:
simp only [hmc, one_mul, modEq_zero_iff] at h

Premises used: Nat.modEq_zero_iff, one_mul
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a b c : ℕ
hmc : c = 1
h : a = b
inl : a ≡ a [MOD 0]
⊢ a ≡ b [MOD 0]

Tactic:
subst h
-- Module: Mathlib.Data.Nat.ModEq
Goal:
a c : ℕ
hmc : c = 1
⊢ a ≡ a [MOD 0]

Tactic:
rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hmc : m.gcd c = 1
h : c * a ≡ c * b [MOD m]
hm : m > 0
⊢ a ≡ b [MOD m]

Tactic:
simpa [hmc] using h.cancel_left_div_gcd hm

Premises used: Nat.ModEq.cancel_left_div_gcd
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m a b c : ℕ
hmc : m.gcd c = 1
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]

Tactic:
simpa [mul_comm] using h

Premises used: mul_comm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n = 0
⊢ a ≡ b [MOD m]

Tactic:
rw [hn, gcd_zero_left] at h

Premises used: Nat.gcd_zero_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : n = 0
h₁ : a ≡ b [MOD m]
⊢ n = 0

Tactic:
rw [hn, gcd_zero_left] at h

Premises used: Nat.gcd_zero_left
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
left : a ≡ a [MOD n]
right : a ≡ b [MOD m]
⊢ a ≡ a [MOD n] ∧ a ≡ b [MOD m]

Tactic:
constructor
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ a [MOD n]

Tactic:
rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]

Tactic:
h
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD m]
hn : n = 0
⊢ a ≡ b [MOD m]

Tactic:
exact h
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : m = 0
⊢ a ≡ b [MOD n]

Tactic:
rw [hm, gcd_zero_right] at h

Premises used: Nat.gcd_zero_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : m = 0
h₁ : a ≡ b [MOD n]
⊢ ¬n = 0

Tactic:
rw [hm, gcd_zero_right] at h

Premises used: Nat.gcd_zero_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : m = 0
h₁ : a ≡ b [MOD n]
hn₁ : ¬n = 0
⊢ m = 0

Tactic:
rw [hm, gcd_zero_right] at h

Premises used: Nat.gcd_zero_right
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
left : b ≡ a [MOD n]
right : b ≡ b [MOD m]
⊢ b ≡ a [MOD n] ∧ b ≡ b [MOD m]

Tactic:
constructor
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n]

Tactic:
h.symm

Premises used: Nat.ModEq.symm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ a [MOD n]

Tactic:
exact h.symm

Premises used: Nat.ModEq.symm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n]
hn : ¬n = 0
hm : m = 0
⊢ b ≡ b [MOD m]

Tactic:
rfl
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
rw :
  (match (motive := ℤ × ℤ → ℕ) (n.gcdA m, n.gcdB m) with
      | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
      a [MOD n] ∧
    (match (motive := ℤ × ℤ → ℕ) (n.gcdA m, n.gcdB m) with
      | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
      b [MOD m]
⊢ (match (motive := ℤ × ℤ → ℕ) n.xgcd m with
      | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
      a [MOD n] ∧
    (match (motive := ℤ × ℤ → ℕ) n.xgcd m with
      | (c, d) => (((↑n : ℤ) * c * (↑b : ℤ) + (↑m : ℤ) * d * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat) ≡
      b [MOD m]

Tactic:
rw [xgcd_val]

Premises used: Nat.xgcd_val
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
rw :
  (↑n : ℤ) ∣
      (↑a : ℤ) -
        ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ) ∧
    (↑m : ℤ) ∣
      (↑b : ℤ) - ((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)
⊢ (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat ≡
      a [MOD n] ∧
    (((↑n : ℤ) * n.gcdA m * (↑b : ℤ) + (↑m : ℤ) * n.gcdB m * (↑a : ℤ)) / (↑(n.gcd m) : ℤ) % (↑(n.lcm m) : ℤ)).toNat ≡
      b [MOD m]

Tactic:
rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]

Premises used: Iff.mpr, Int.natCast_ne_zero, Int.toNat_of_nonneg, Nat.modEq_iff_dvd, Nat.lcm_ne_zero, Int.emod_nonneg
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
norm_cast : ¬n.gcd m = 0
⊢ Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0

Tactic:
norm_cast
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
rw : n = 0 → ¬m = 0
⊢ ¬n.gcd m = 0

Tactic:
rw [Nat.gcd_eq_zero_iff, not_and]

Premises used: not_and, Nat.gcd_eq_zero_iff
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ n = 0 → ¬m = 0

Tactic:
fun _ => hm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ n = 0 → ¬m = 0

Tactic:
exact fun _ => hm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
⊢ Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0

Tactic:
have hnonzero : (gcd n m : ℤ) ≠ 0 := by
          norm_cast
          rw [Nat.gcd_eq_zero_iff, not_and]
          exact fun _ => hm
-- Module: Mathlib.Data.Nat.ModEq
Goal:
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : Ne (α := ℤ) (↑(n.gcd m) : ℤ) 0
⊢ ∀ (t : ℤ), (↑(n.gcd m) : ℤ) ∣ t * HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)

Tactic:
have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _