# Zulip Chat Archive

## Stream: new members

### Topic: Real.sqrt

#### Adhithi Varadarajan⚛️ (Jul 28 2023 at 22:12):

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.

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

Could your fix your code using (the right) #backticks please?

#### 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