## Stream: new members

### Topic: Real.sqrt

Hello, I was working with square root of numbers to prove a theorem. I was trying to prove that the square root of a number squared is the number itself. I am unable to come up with any tactic to solve the goal. Do you have any ideas? Thank you.

'''
import Mathlib.Data.Real.Sqrt

example { p : ℝ} (h1: p>0) :
p= Real.sqrt (p^2) :=
calc
p= p := by ring
_= Real.sqrt ((p)^2) := by ring

'''
Square roots usually give you two solutions and I was wondering if we could ensure that the codes accepted the positive root.

#### Peter Hansen (Jul 28 2023 at 22:22):

This is true for any positive real number including zero.

import Mathlib.Data.Real.Sqrt

example {p : ℝ} (h1: 0 ≤ p) : p = Real.sqrt (p^2) :=
calc
p = p := by ring
_ = Real.sqrt ((p)^2) := symm (Real.sqrt_sq h1)


#### Anatole Dedecker (Jul 28 2023 at 22:24):

Indeed here you're not looking for a tactic but for a result in the library, and docs#Real.sqrt_sq is that result.

#### Patrick Massot (Jul 28 2023 at 22:25):

Peter's answer is probably correct but can be shorten a lot:

import Mathlib.Data.Real.Sqrt

example {p : ℝ} (h1: 0 ≤ p) : p = Real.sqrt (p^2) :=
(Real.sqrt_sq h1).symm


#### Scott Morrison (Jul 29 2023 at 03:45):

And of course:

import Mathlib.Data.Real.Sqrt

example {p : ℝ} (h1: 0 ≤ p) : p = Real.sqrt (p^2) := by exact?


is the canonical way to find this lemma.

Last updated: Dec 20 2023 at 11:08 UTC