[GOAL]
q : ℚ
⊢ sqrt (q * q) = |q|
[PROOFSTEP]
rw [sqrt, mul_self_num, mul_self_den, Int.sqrt_eq, Nat.sqrt_eq, abs_def, divInt_ofNat]
[GOAL]
x : ℚ
x✝ : ∃ q, q * q = x
n : ℚ
hn : n * n = x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [← hn, sqrt_eq, abs_mul_abs_self]
