m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
m n a b c d : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
letI d := gcd m c
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
have hmd := gcd_dvd_left m c
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
have hcd := gcd_dvd_right m c
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑(gcd m c) ∣ b - a
m n a b c d✝ : ℤ
hm : 0 < m
h : a * c ≡ b * c [ZMOD m]
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ a ≡ b [ZMOD m / ↑(gcd m c)]
rw [modEq_iff_dvd] at h ⊢
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ c / ↑d * (b - a)

case refine_2
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ gcd (m / ↑(gcd m c)) (c / ↑d) = 1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑(gcd m c) ∣ b - a
refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(gcd m c)
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ c / ↑d * (b - a)
rw [mul_comm, ← Int.mul_ediv_assoc (b - a) hcd, sub_mul]
no goals
case refine_1
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ m / ↑d ∣ (b * c - a * c) / ↑(gcd m c)
exact Int.ediv_dvd_ediv hmd h
no goals
case refine_2
m n a b c d✝ : ℤ
hm : 0 < m
h : m ∣ b * c - a * c
d : ℕ := gcd m c
hmd : ↑(gcd m c) ∣ m
hcd : ↑(gcd m c) ∣ c
⊢ gcd (m / ↑(gcd m c)) (c / ↑d) = 1
rw [gcd_div hmd hcd, natAbs_ofNat, Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]