[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0 : m = 0
⊢ m ∣ n
[PROOFSTEP]
simp [m0] at ae 
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
m0 : m = 0
ae : n = 0
⊢ m ∣ n
[PROOFSTEP]
simp [ae, m0]
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ m ∣ n
[PROOFSTEP]
cases' eq_ofNat_of_zero_le (@nonneg_of_mul_nonneg_right ℤ _ m a (by simp [ae.symm]) (by simpa using m0l)) with k e
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ 0 ≤ ↑m * a
[PROOFSTEP]
simp [ae.symm]
[GOAL]
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
⊢ 0 < ↑m
[PROOFSTEP]
simpa using m0l
[GOAL]
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
a : ℤ
ae : ↑n = ↑m * a
m0l : m > 0
k : ℕ
e : a = ↑k
⊢ m ∣ n
[PROOFSTEP]
subst a
[GOAL]
case intro
m n : ℕ
x✝ : ↑m ∣ ↑n
m0l : m > 0
k : ℕ
ae : ↑n = ↑m * ↑k
⊢ m ∣ n
[PROOFSTEP]
exact ⟨k, Int.ofNat.inj ae⟩
[GOAL]
m n : ℕ
x✝ : m ∣ n
k : ℕ
e : n = m * k
⊢ ↑m * ↑k = ↑n
[PROOFSTEP]
rw [e, Int.ofNat_mul]
[GOAL]
n : ℕ
z : ℤ
⊢ ↑n ∣ z ↔ n ∣ natAbs z
[PROOFSTEP]
rcases natAbs_eq z with (eq | eq)
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ ↑n ∣ z ↔ n ∣ natAbs z
[PROOFSTEP]
rw [eq]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ ↑n ∣ z ↔ n ∣ natAbs z
[PROOFSTEP]
rw [eq]
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ ↑n ∣ ↑(natAbs z) ↔ n ∣ natAbs ↑(natAbs z)
[PROOFSTEP]
simp [← coe_nat_dvd]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ ↑n ∣ -↑(natAbs z) ↔ n ∣ natAbs (-↑(natAbs z))
[PROOFSTEP]
simp [← coe_nat_dvd]
[GOAL]
n : ℕ
z : ℤ
⊢ z ∣ ↑n ↔ natAbs z ∣ n
[PROOFSTEP]
rcases natAbs_eq z with (eq | eq)
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ z ∣ ↑n ↔ natAbs z ∣ n
[PROOFSTEP]
rw [eq]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ z ∣ ↑n ↔ natAbs z ∣ n
[PROOFSTEP]
rw [eq]
[GOAL]
case inl
n : ℕ
z : ℤ
eq : z = ↑(natAbs z)
⊢ ↑(natAbs z) ∣ ↑n ↔ natAbs ↑(natAbs z) ∣ n
[PROOFSTEP]
simp [← coe_nat_dvd]
[GOAL]
case inr
n : ℕ
z : ℤ
eq : z = -↑(natAbs z)
⊢ -↑(natAbs z) ∣ ↑n ↔ natAbs (-↑(natAbs z)) ∣ n
[PROOFSTEP]
simp [← coe_nat_dvd]
