Is there a code for extracting square root?

Stream: Is there code for X?

[Shi You]

Something like

variable (x : ℚ)
example (h: x ^ 2 = 9): x = 3 ∨ x = -3 := by extract_sq_root

[Mario Carneiro]

that's just a lemma: look for x ^ 2 = y ^ 2 <-> x = y \/ x = -y

[Shi You]

It doesn't automatically change 9 to 3^2?

[Mario Carneiro]

norm_num will do that part

[Mario Carneiro]

import tactic
variable (x : ℚ)
example (h: x ^ 2 = 9) : x = 3 ∨ x = -3 :=
eq_or_eq_neg_of_sq_eq_sq _ _ $ by norm_num [h]