rw [Real.sqrt_sq_eq_abs] at hsq
case h.mp
x : ℝ
hsq : Real.sqrt (x ^ 2) = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
case h.mp
x : ℝ
hsq : |x| = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17