case intro
a b c d : ℤ
hb : b ≠ 0
h : b * a = c * d
k : ℤ
hk : c = b * k
⊢ a = c / b * d
a b c d : ℤ
hb : b ≠ 0
hbc : b ∣ c
h : b * a = c * d
⊢ a = c / b * d
cases' hbc with k hk
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d
case intro
a b c d : ℤ
hb : b ≠ 0
h : b * a = c * d
k : ℤ
hk : c = b * k
⊢ a = c / b * d
subst hk
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = b * k / b * d
rw [Int.mul_ediv_cancel_left _ hb]
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * (k * d)
⊢ a = k * d
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * k * d
⊢ a = k * d
rw [mul_assoc] at h
no goals
case intro
a b d : ℤ
hb : b ≠ 0
k : ℤ
h : b * a = b * (k * d)
⊢ a = k * d
apply mul_left_cancel₀ hb h