have h1 : b ^ 2 ∣ a ^ 2 := by simp_all only [ne_eq, dvd_mul_right]
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
⊢ ∃ d, c = d ^ 2
a b c : ℤ
hb : b ≠ 0
h : a ^ 2 = b ^ 2 * c
h1 : b ^ 2 ∣ a ^ 2
⊢ ∃ d, c = d ^ 2