rw [mul_pow, mul_right_inj' (by positivity)] at h
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : (b * d) ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2
case intro
b c : ℤ
hb : b ≠ 0
d : ℤ
h : d ^ 2 = c
h1 : b ^ 2 ∣ (b * d) ^ 2
⊢ ∃ d, c = d ^ 2