d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(Int.natAbs x * Int.natAbs x) = ↑(d * Int.natAbs y * Int.natAbs y)
⊢ x = 0 ∧ y = 0
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : x * x = ↑d * y * y
⊢ x = 0 ∧ y = 0
rw [mul_assoc, ← Int.natAbs_mul_self, ← Int.natAbs_mul_self, ← Int.ofNat_mul, ← mul_assoc] at h
no goals
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(Int.natAbs x * Int.natAbs x) = ↑(d * Int.natAbs y * Int.natAbs y)
⊢ x = 0 ∧ y = 0
exact
  let ⟨h1, h2⟩ := divides_sq_eq_zero (Int.ofNat.inj h)
  ⟨Int.natAbs_eq_zero.mp h1, Int.natAbs_eq_zero.mp h2⟩