i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
⊢ i ∣ j
i j k : ℤ
k_non_zero : k ≠ 0
H : i * k ∣ j * k
⊢ i ∣ j
rw [mul_comm i k, mul_comm j k] at H
no goals
i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
⊢ i ∣ j
exact dvd_of_mul_dvd_mul_left k_non_zero H