Real.sqrt

Stream: new members

[Adhithi Varadarajan⚛️]

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]

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

[Peter Hansen]

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]

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]

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]

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.