case pos
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : abs x < m
hm : m = 0
⊢ x = 0

case neg
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : abs x < m
hm : ¬m = 0
⊢ x = 0
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : abs x < m
⊢ x = 0
by_cases hm : m = 0
case neg.intro
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : abs (m * d) < m
⊢ m * d = 0
case neg
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : abs x < m
hm : ¬m = 0
⊢ x = 0
rcases h1 with ⟨d, rfl⟩
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : abs (m * d) < m
⊢ d = 0
case neg.intro
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : abs (m * d) < m
⊢ m * d = 0
apply mul_eq_zero_of_right
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : abs (m * d) < m
⊢ abs (m * d) < abs m
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : abs (m * d) < m
⊢ d = 0
rw [← abs_lt_one_iff, ← mul_lt_iff_lt_one_right (abs_pos.mpr hm), ← abs_mul]
no goals
case neg.intro.h
a b : ℤ
n : ℕ
m : ℤ
hm : ¬m = 0
d : ℤ
h2 : abs (m * d) < m
⊢ abs (m * d) < abs m
exact lt_of_lt_of_le h2 (le_abs_self m)
case pos
a b : ℤ
n : ℕ
x : ℤ
h1 : 0 ∣ x
h2 : abs x < 0
⊢ x = 0
case pos
a b : ℤ
n : ℕ
m x : ℤ
h1 : m ∣ x
h2 : abs x < m
hm : m = 0
⊢ x = 0
subst m
no goals
case pos
a b : ℤ
n : ℕ
x : ℤ
h1 : 0 ∣ x
h2 : abs x < 0
⊢ x = 0
exact zero_dvd_iff.mp h1