i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
l : ℤ
H1 : k * j = k * (i * l)
⊢ i ∣ j
i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
l : ℤ
H1 : k * j = k * i * l
⊢ i ∣ j
rw [mul_assoc] at H1
no goals
i j k : ℤ
k_non_zero : k ≠ 0
H : k * i ∣ k * j
l : ℤ
H1 : k * j = k * (i * l)
⊢ i ∣ j
exact ⟨_, mul_left_cancel₀ k_non_zero H1⟩