m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : m ∣ Int.natAbs (↑b - ↑a) ∧ n ∣ Int.natAbs (↑b - ↑a)
⊢ a ≡ b [MOD m * n]
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]
rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd, ← Int.dvd_natAbs,
  Int.coe_nat_dvd] at h
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : m ∣ Int.natAbs (↑b - ↑a) ∧ n ∣ Int.natAbs (↑b - ↑a)
⊢ m * n ∣ Int.natAbs (↑b - ↑a)
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : m ∣ Int.natAbs (↑b - ↑a) ∧ n ∣ Int.natAbs (↑b - ↑a)
⊢ a ≡ b [MOD m * n]
rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.coe_nat_dvd]
no goals
m✝ n✝ a✝ b✝ c d a b m n : ℕ
hmn : coprime m n
h : m ∣ Int.natAbs (↑b - ↑a) ∧ n ∣ Int.natAbs (↑b - ↑a)
⊢ m * n ∣ Int.natAbs (↑b - ↑a)
exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2