rw [mul_pow, mul_comm, mul_right_inj' (pow_ne_zero _ hb)] at h
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a * b ^ 2 = (b * k) ^ 2
⊢ IsSquare a
case inr.intro
a b : ℤ
hb : b ≠ 0
k : ℤ
h : a = k ^ 2
⊢ IsSquare a