[GOAL]
n : ℤ
⊢ sqrt (n * n) = ↑(natAbs n)
[PROOFSTEP]
rw [sqrt, ← natAbs_mul_self, toNat_coe_nat, Nat.sqrt_eq]
[GOAL]
x : ℤ
x✝ : ∃ n, n * n = x
n : ℤ
hn : n * n = x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [← hn, sqrt_eq, ← Int.ofNat_mul, natAbs_mul_self]
