rw [Int.pow_dvd_pow_iff two_ne_zero] at h1
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ^ 2 ∣ c ^ 2
⊢ IsSquare a
case inr
a b c : ℤ
h : a * b ^ 2 = c ^ 2
hb : b ≠ 0
h1 : b ∣ c
⊢ IsSquare a