apply_fun (λ eq => Real.sqrt eq) at hsq
case h.mp
x : ℝ
hsq : x ^ 2 = 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17
case h.mp
x : ℝ
hsq : Real.sqrt (x ^ 2) = Real.sqrt 17
⊢ x = Real.sqrt 17 ∨ x = -Real.sqrt 17