a b : Int
x✝ : natAbs a ∣ natAbs b
k : Nat
hk : natAbs b = natAbs a * k
⊢ a ∣ b
a b : Int
⊢ natAbs a ∣ natAbs b ↔ a ∣ b
refine ⟨fun ⟨k, hk⟩ => ?_, fun ⟨k, hk⟩ => ⟨natAbs k, hk.symm ▸ natAbs_mul a k⟩⟩
a b : Int
x✝ : natAbs a ∣ natAbs b
k : Nat
hk : b = a * ↑k ∨ b = -(a * ↑k)
⊢ a ∣ b
a b : Int
x✝ : natAbs a ∣ natAbs b
k : Nat
hk : natAbs b = natAbs a * k
⊢ a ∣ b
rw [← natAbs_ofNat k, ← natAbs_mul, natAbs_eq_natAbs_iff] at hk
case inl
a : Int
k : Nat
x✝ : natAbs a ∣ natAbs (a * ↑k)
⊢ a ∣ a * ↑k

case inr
a : Int
k : Nat
x✝ : natAbs a ∣ natAbs (-(a * ↑k))
⊢ a ∣ -(a * ↑k)
a b : Int
x✝ : natAbs a ∣ natAbs b
k : Nat
hk : b = a * ↑k ∨ b = -(a * ↑k)
⊢ a ∣ b
cases hk <;> subst b
no goals
case inl
a : Int
k : Nat
x✝ : natAbs a ∣ natAbs (a * ↑k)
⊢ a ∣ a * ↑k
apply Int.dvd_mul_right
case inr
a : Int
k : Nat
x✝ : natAbs a ∣ natAbs (-(a * ↑k))
⊢ a ∣ a * -↑k
case inr
a : Int
k : Nat
x✝ : natAbs a ∣ natAbs (-(a * ↑k))
⊢ a ∣ -(a * ↑k)
rw [← Int.mul_neg]
no goals
case inr
a : Int
k : Nat
x✝ : natAbs a ∣ natAbs (-(a * ↑k))
⊢ a ∣ a * -↑k
apply Int.dvd_mul_right