awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) ↔ x ≤ y

Tactic:
sqrt.le_iff_le

Premises used: OrderIso.le_iff_le, NNReal.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ LT.lt (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) ↔ x < y

Tactic:
sqrt.lt_iff_lt

Premises used: OrderIso.lt_iff_lt, NNReal.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) x = y ↔ x = HPow.hPow (β := ℕ) y 2

Tactic:
sqrt.toEquiv.apply_eq_iff_eq_symm_apply

Premises used: Function.invFun, dite, NNReal.sqrt, RelIso.toEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2

Tactic:
sqrt.to_galoisConnection _ _

Premises used: OrderIso.to_galoisConnection, NNReal.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) y ↔ HPow.hPow (β := ℕ) x 2 ≤ y

Tactic:
(sqrt.symm.to_galoisConnection _ _).symm

Premises used: Function.invFun, OrderIso.to_galoisConnection, OrderIso.symm, dite, NNReal.sqrt, Iff.symm
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0) ↔ x = 0

Tactic:
simp [sqrt_eq_iff_eq_sq]

Premises used: NNReal.sqrt_eq_iff_eq_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ↔ x = 1

Tactic:
simp [sqrt_eq_iff_eq_sq]

Premises used: NNReal.sqrt_eq_iff_eq_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 0) 0

Tactic:
simp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1) 1

Tactic:
simp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
rw :
  LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ↔
    x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
rw₁ : x ≤ 1 ↔ x ≤ (sqrt : (a : ℝ≥0) → ℝ≥0) 1
rw₂ rw₃ : x ≤ 1 ↔ x ≤ 1
⊢ LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0) ↔ x ≤ 1

Tactic:
rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]

Premises used: NNReal.sqrt_le_sqrt, NNReal.sqrt_one
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
rw :
  LE.le (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) 1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔
    (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
rw₁ : 1 ≤ x ↔ (sqrt : (a : ℝ≥0) → ℝ≥0) 1 ≤ x
rw₂ rw₃ : 1 ≤ x ↔ 1 ≤ x
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔ 1 ≤ x

Tactic:
rw [← sqrt_one, sqrt_le_sqrt, sqrt_one]

Premises used: NNReal.sqrt_le_sqrt, NNReal.sqrt_one
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
rw : x * y ≤ max x y * max x y
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) ≤ max x y

Tactic:
rw [sqrt_le_iff_le_sq, sq]

Premises used: NNReal.sqrt_le_iff_le_sq, sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
h₁ : x ≤ max x y
h₂ : y ≤ max x y
⊢ x * y ≤ max x y * max x y

Tactic:
gcongr
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ x ≤ max x y

Tactic:
simp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ y ≤ max x y

Tactic:
simp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
rw :
  x * y =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)) 2
rw₁ :
  x * y =
    HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) 2 *
      HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
rw₂ : x * y = x * HPow.hPow (α := ℝ≥0) (β := ℕ) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0) 2
rw₃ rw₄ : x * y = x * y
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x * y) =
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)

Tactic:
rw [sqrt_eq_iff_eq_sq, mul_pow, sq_sqrt, sq_sqrt]

Premises used: NNReal.sqrt_eq_iff_eq_sq, mul_pow, NNReal.sq_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ Eq (α := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x⁻¹ : ℝ≥0) (((sqrt : (a : ℝ≥0) → ℝ≥0) x)⁻¹ : ℝ≥0)

Tactic:
map_inv₀ sqrtHom x

Premises used: map_inv₀, NNReal.sqrtHom
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ≥0
⊢ (sqrt : (a : ℝ≥0) → ℝ≥0) (x / y) =
    HDiv.hDiv (α := ℝ≥0) (β := ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) y : ℝ≥0)

Tactic:
map_div₀ sqrtHom x y

Premises used: map_div₀, NNReal.sqrtHom
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ Continuous (X := ℝ≥0) (Y := ℝ≥0) (⇑sqrt : (a : ℝ≥0) → ℝ≥0)

Tactic:
sqrt.continuous

Premises used: OrderIso.continuous, NNReal.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((sqrt : (a : ℝ≥0) → ℝ≥0) x : ℝ≥0) ↔ 0 < x

Tactic:
simp [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
⊢ IsSquare x

Tactic:
⟨_, mul_self_sqrt _ |>.symm⟩

Premises used: NNReal.mul_self_sqrt, IsSquare, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ≥0
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) (↑x : ℝ).toNNReal) : ℝ)
rw₁ rw₂ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ)
⊢ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x) : ℝ) = √(↑x : ℝ)

Tactic:
rw [Real.sqrt, Real.toNNReal_coe]

Premises used: Real.toNNReal_coe, Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
unfold : Continuous (Y := ℝ) fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ √x

Tactic:
unfold sqrt

Premises used: Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Data.Real.Sqrt
Goal:
unfold : Eq (α := Filter ℝ) (map (fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)) atTop) atTop
⊢ Eq (α := Filter ℝ) (map (fun (x : ℝ) ↦ √x) atTop) atTop

Tactic:
unfold sqrt

Premises used: Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ map (NNReal.toReal ∘ (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) ∘ toNNReal) atTop = atTop

Tactic:
simp [← map_map]

Premises used: Filter.map_map
-- Module: Mathlib.Data.Real.Sqrt
Goal:
unfold :
  Eq (α := Filter ℝ) (comap (β := ℝ) (fun (x : ℝ) ↦ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)) atTop) atTop
⊢ Eq (α := Filter ℝ) (comap (β := ℝ) (fun (x : ℝ) ↦ √x) atTop) atTop

Tactic:
unfold sqrt

Premises used: Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ comap (NNReal.toReal ∘ (⇑NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) ∘ toNNReal) atTop = atTop

Tactic:
simp [← comap_comap]

Premises used: Filter.comap_comap
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ √x) atTop atTop

Tactic:
map_sqrt_atTop.le

Premises used: Real.map_sqrt_atTop, Eq.le, Filter.Tendsto
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : x ≤ 0
⊢ √x = 0

Tactic:
simp [sqrt, Real.toNNReal_eq_zero.2 h]

Premises used: Iff.mpr, Real.toNNReal_eq_zero, Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
unfold : 0 ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)
⊢ 0 ≤ √x

Tactic:
unfold sqrt

Premises used: Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
⊢ 0 ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)

Tactic:
NNReal.coe_nonneg _

Premises used: NNReal.coe_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
⊢ 0 ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ)

Tactic:
exact NNReal.coe_nonneg _

Premises used: NNReal.coe_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 ≤ x
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) * (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = x
rw₁ :
  (↑(HMul.hMul (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
          ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)) :
      ℝ) =
    x
rw₂ : (↑x.toNNReal : ℝ) = x
rw₃ rw₄ : x = x
⊢ √x * √x = x

Tactic:
rw [Real.sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]

Premises used: NNReal.mul_self_sqrt, Real.coe_toNNReal, Real.sqrt, NNReal.coe_mul
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 ≤ x
⊢ √(x * x) = x

Tactic:
(mul_self_inj_of_nonneg (sqrt_nonneg _) h).1 (mul_self_sqrt (mul_self_nonneg _))

Premises used: mul_self_nonneg, mul_self_inj_of_nonneg, Real.mul_self_sqrt, Iff.mp, Real.sqrt_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
mp : √x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
mpr : y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → √x = y
⊢ √x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0

Tactic:
constructor
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
mp : ∀ (hle : 0 ≤ x), √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
mp₁ : ∀ (hlt : x < 0), √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
rcases le_or_gt 0 x with hle | hlt

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩

Premises used: Real.mul_self_sqrt, And.intro, Or.inl, Real.sqrt_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩

Premises used: Or.inl
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩

Premises used: Real.sqrt_eq_zero_of_nonpos, LT.lt.le, And.intro, Or.inr
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
hlt : x < 0
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩

Premises used: Or.inr
-- Module: Mathlib.Data.Real.Sqrt
Goal:
y : ℝ
hy : 0 ≤ y
⊢ √(y * y) = y

Tactic:
sqrt_mul_self hy

Premises used: Real.sqrt_mul_self
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
hx : x < 0
⊢ √x = 0

Tactic:
sqrt_eq_zero_of_nonpos hx.le

Premises used: Real.sqrt_eq_zero_of_nonpos, LT.lt.le
-- Module: Mathlib.Data.Real.Sqrt
Goal:
y : ℝ
hy : 0 ≤ y
⊢ √(y * y) = y

Tactic:
exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]

Premises used: Real.sqrt_mul_self
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : √x = y
rw : x = √x * √x
rw₁ rw₂ : x = x
⊢ x = y * y

Tactic:
rw [← h, mul_self_sqrt hx]

Premises used: Real.mul_self_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : x = y * y
rw : √(y * y) = y
rw₁ rw₂ : y = y
⊢ √x = y

Tactic:
rw [h, sqrt_mul_self hy]

Premises used: Real.sqrt_mul_self
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : 0 < y
⊢ √x = y ↔ y * y = x

Tactic:
simp [sqrt_eq_cases, h.ne', h.le]

Premises used: Real.sqrt_eq_cases, LT.lt.le, LT.lt.ne'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : x = HMul.hMul (α := ℝ) 1 1 ↔ x = 1
rw₁ rw₂ : x = 1 ↔ x = 1
⊢ HMul.hMul (α := ℝ) 1 1 = x ↔ x = 1

Tactic:
rw [eq_comm, mul_one]

Premises used: eq_comm, mul_one
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 ≤ x
rw : √x * √x = x
rw₁ rw₂ : x = x
⊢ HPow.hPow (β := ℕ) (√x) 2 = x

Tactic:
rw [sq, mul_self_sqrt h]

Premises used: Real.mul_self_sqrt, sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 ≤ x
rw : √(x * x) = x
rw₁ rw₂ : x = x
⊢ √(HPow.hPow (β := ℕ) x 2) = x

Tactic:
rw [sq, sqrt_mul_self h]

Premises used: Real.sqrt_mul_self, sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
rw : √x = y ↔ x = y * y
rw₁ rw₂ : x = y * y ↔ x = y * y
⊢ √x = y ↔ x = HPow.hPow (β := ℕ) y 2

Tactic:
rw [sq, sqrt_eq_iff_mul_self_eq hx hy]

Premises used: sq, Real.sqrt_eq_iff_mul_self_eq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : √(|x| * |x|) = |x|
rw₁ rw₂ : |x| = |x|
⊢ √(x * x) = |x|

Tactic:
rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]

Premises used: Real.sqrt_mul_self, abs_mul_abs_self, abs_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : √(x * x) = |x|
rw₁ rw₂ : |x| = |x|
⊢ √(HPow.hPow (β := ℕ) x 2) = |x|

Tactic:
rw [sq, sqrt_mul_self_eq_abs]

Premises used: sq, Real.sqrt_mul_self_eq_abs
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ √0 = 0

Tactic:
simp [Real.sqrt]

Premises used: Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ √1 = 1

Tactic:
simp [Real.sqrt]

Premises used: Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ √y ↔ x ≤ y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x ≤ y
rw₂ :
  LE.le (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
    x ≤ y
rw₃ : x.toNNReal ≤ y.toNNReal ↔ x ≤ y
rw₄ rw₅ : x ≤ y ↔ x ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt, toNNReal_le_toNNReal_iff hy]

Premises used: NNReal.sqrt_le_sqrt, Real.toNNReal_le_toNNReal_iff, Real.sqrt, NNReal.coe_le_coe
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
⊢ √x < √y ↔ x < y

Tactic:
lt_iff_lt_of_le_iff_le (sqrt_le_sqrt_iff hx)

Premises used: Real.sqrt_le_sqrt_iff, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hy : 0 < y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < √y ↔ x < y
rw₁ : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) < (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal) : ℝ) ↔ x < y
rw₂ :
  LT.lt (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) y.toNNReal : ℝ≥0) ↔
    x < y
rw₃ : x.toNNReal < y.toNNReal ↔ x < y
rw₄ rw₅ : x < y ↔ x < y
⊢ √x < √y ↔ x < y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]

Premises used: Real.toNNReal_lt_toNNReal_iff, NNReal.coe_lt_coe, Real.sqrt, NNReal.sqrt_lt_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : x ≤ y
rw : x.toNNReal ≤ y.toNNReal
⊢ √x ≤ √y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt]

Premises used: NNReal.sqrt_le_sqrt, Real.sqrt, NNReal.coe_le_coe
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal

Tactic:
toNNReal_le_toNNReal h

Premises used: Real.toNNReal_le_toNNReal
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : x ≤ y
⊢ x.toNNReal ≤ y.toNNReal

Tactic:
exact toNNReal_le_toNNReal h

Premises used: Real.toNNReal_le_toNNReal
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ Monotone sqrt

Tactic:
fun _ _ ↦ sqrt_le_sqrt

Premises used: Monotone, Real.sqrt_le_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ StrictMonoOn sqrt (Ici 0)

Tactic:
fun _ ha _ _ h => (sqrt_lt_sqrt_iff ha).mpr h

Premises used: Iff.mpr, Real.sqrt_lt_sqrt_iff, StrictMonoOn
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
h : x < y
⊢ √x < √y

Tactic:
(sqrt_lt_sqrt_iff hx).2 h

Premises used: Iff.mpr, Real.sqrt_lt_sqrt_iff
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₁ : (NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal ≤ y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₂ : x.toNNReal ≤ HPow.hPow (β := ℕ) y.toNNReal 2 ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₃ : x.toNNReal ≤ y.toNNReal * y.toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₄ : x.toNNReal ≤ (y * y).toNNReal ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₅ : x ≤ y * y ↔ x ≤ HPow.hPow (β := ℕ) y 2
rw₆ rw₇ : x ≤ y * y ↔ x ≤ y * y
⊢ √x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2

Tactic:
rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff_le_sq, sq, ← Real.toNNReal_mul hy,
    Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]

Premises used: mul_self_nonneg, Real.toNNReal_mul, NNReal.sqrt_le_iff_le_sq, Real.le_toNNReal_iff_coe_le, Real.toNNReal_le_toNNReal_iff, sq, Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
rw : 0 ≤ y → (√x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2)
⊢ √x ≤ y ↔ 0 ≤ y ∧ x ≤ HPow.hPow (β := ℕ) y 2

Tactic:
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]

Premises used: and_congr_right_iff, LE.le.trans, Real.sqrt_nonneg, and_iff_right_of_imp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2)

Tactic:
sqrt_le_left

Premises used: Real.sqrt_le_left
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
⊢ 0 ≤ y → (√x ≤ y ↔ x ≤ HPow.hPow (β := ℕ) y 2)

Tactic:
exact sqrt_le_left

Premises used: Real.sqrt_le_left
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
rw : √x < y ↔ √x < √(HPow.hPow (β := ℕ) y 2)
rw₁ rw₂ : √x < y ↔ √x < y
⊢ √x < y ↔ x < HPow.hPow (β := ℕ) y 2

Tactic:
rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]

Premises used: Real.sqrt_lt_sqrt_iff, Real.sqrt_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hy : 0 < y
rw : √x < y ↔ √x < √(HPow.hPow (β := ℕ) y 2)
rw₁ rw₂ : √x < y ↔ √x < y
⊢ √x < y ↔ x < HPow.hPow (β := ℕ) y 2

Tactic:
rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]

Premises used: pow_pos, Real.sqrt_lt_sqrt_iff_of_pos, LT.lt.le, Real.sqrt_sq
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ x ≤ √y ↔ HPow.hPow (β := ℕ) x 2 ≤ y

Tactic:
le_iff_le_iff_lt_iff_lt.2 <| sqrt_lt hy hx

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Real.sqrt_lt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 < x
⊢ x ≤ √y ↔ HPow.hPow (β := ℕ) x 2 ≤ y

Tactic:
le_iff_le_iff_lt_iff_lt.2 <| sqrt_lt' hx

Premises used: Iff.mpr, le_iff_le_iff_lt_iff_lt, Real.sqrt_lt'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 ≤ y
rw : √(HPow.hPow (β := ℕ) x 2) ≤ √y
⊢ |x| ≤ √y

Tactic:
rw [← sqrt_sq_eq_abs]

Premises used: Real.sqrt_sq_eq_abs
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 ≤ y
⊢ √(HPow.hPow (β := ℕ) x 2) ≤ √y

Tactic:
sqrt_le_sqrt h

Premises used: Real.sqrt_le_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 ≤ y
⊢ √(HPow.hPow (β := ℕ) x 2) ≤ √y

Tactic:
exact sqrt_le_sqrt h

Premises used: Real.sqrt_le_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : 0 ≤ y
mp : HPow.hPow (β := ℕ) x 2 ≤ y → -√y ≤ x ∧ x ≤ √y
mpr : -√y ≤ x ∧ x ≤ √y → HPow.hPow (β := ℕ) x 2 ≤ y
⊢ HPow.hPow (β := ℕ) x 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y

Tactic:
constructor
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : 0 ≤ y
⊢ HPow.hPow (β := ℕ) x 2 ≤ y → -√y ≤ x ∧ x ≤ √y

Tactic:
simpa only [abs_le] using abs_le_sqrt

Premises used: abs_le, Real.abs_le_sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : 0 ≤ y
mpr : |x| ≤ √y → HPow.hPow (β := ℕ) |x| 2 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → HPow.hPow (β := ℕ) x 2 ≤ y

Tactic:
rw [← abs_le, ← sq_abs]

Premises used: abs_le, sq_abs
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ √y → HPow.hPow (β := ℕ) |x| 2 ≤ y

Tactic:
(le_sqrt (abs_nonneg x) h).mp

Premises used: Real.le_sqrt, Iff.mp, abs_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ √y → HPow.hPow (β := ℕ) |x| 2 ≤ y

Tactic:
exact (le_sqrt (abs_nonneg x) h).mp

Premises used: Real.le_sqrt, Iff.mp, abs_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 ≤ y
⊢ -√y ≤ x

Tactic:
((sq_le ((sq_nonneg x).trans h)).mp h).1

Premises used: Real.sq_le, And.left, sq_nonneg, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
h : HPow.hPow (β := ℕ) x 2 ≤ y
⊢ x ≤ √y

Tactic:
((sq_le ((sq_nonneg x).trans h)).mp h).2

Premises used: Real.sq_le, And.right, sq_nonneg, Iff.mp, LE.le.trans
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = √y ↔ x = y

Tactic:
simp [le_antisymm_iff, hx, hy]

Premises used: le_antisymm_iff
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 ≤ x
⊢ √x = 0 ↔ x = 0

Tactic:
simpa using sqrt_inj h le_rfl

Premises used: le_rfl, Real.sqrt_inj
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : (↑((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal) : ℝ) = 0 ↔ x ≤ 0
rw₁ : Eq (α := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) x.toNNReal : ℝ≥0) (0 : ℝ≥0) ↔ x ≤ 0
rw₂ : x.toNNReal = 0 ↔ x ≤ 0
rw₃ rw₄ : x ≤ 0 ↔ x ≤ 0
⊢ √x = 0 ↔ x ≤ 0

Tactic:
rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]

Premises used: NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero, Real.sqrt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 ≤ x
rw : √x = 0 ↔ x = 0
rw₁ rw₂ : x = 0 ↔ x = 0
⊢ √x ≠ 0 ↔ x ≠ 0

Tactic:
rw [not_iff_not, sqrt_eq_zero h]

Premises used: not_iff_not, Real.sqrt_eq_zero
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : √x ≠ 0 ↔ ¬x ≤ 0
rw₁ : √x = 0 ↔ x ≤ 0
rw₂ rw₃ : x ≤ 0 ↔ x ≤ 0
⊢ √x ≠ 0 ↔ 0 < x

Tactic:
rw [← not_le, not_iff_not, sqrt_eq_zero']

Premises used: not_le, not_iff_not, Real.sqrt_eq_zero'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
inl : x < 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
inr : x = 0 → HPow.hPow (β := ℕ) (√x) 2 = max x 0
inr₁ : 0 < x → HPow.hPow (β := ℕ) (√x) 2 = max x 0
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0

Tactic:
rcases lt_trichotomy x 0 with _ | _ | _

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : x < 0
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0

Tactic:
grind [sqrt_eq_zero', sq_sqrt]

Premises used: Real.sq_sqrt, Real.sqrt_eq_zero'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : x = 0
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0

Tactic:
grind [sqrt_eq_zero', sq_sqrt]

Premises used: Real.sq_sqrt, Real.sqrt_eq_zero'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
h : 0 < x
⊢ HPow.hPow (β := ℕ) (√x) 2 = max x 0

Tactic:
grind [sqrt_eq_zero', sq_sqrt]

Premises used: Real.sq_sqrt, Real.sqrt_eq_zero'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
⊢ √7 ≠ 0

Tactic:
grind
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
⊢ √x ≤ 0 ↔ √x = 0

Tactic:
simp [le_antisymm_iff, sqrt_nonneg]

Premises used: le_antisymm_iff, Real.sqrt_nonneg
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 < x
inl : ∀ (hy : y ≤ 0), √x ≤ √y ↔ x ≤ y
inr : ∀ (hy : 0 ≤ y), √x ≤ √y ↔ x ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
obtain hy | hy := le_total y 0

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
iff_of_false ((sqrt_eq_zero_of_nonpos hy).trans_lt <| sqrt_pos.2 hx).not_ge
      (hy.trans_lt hx).not_ge

Premises used: Iff.mpr, Real.sqrt_eq_zero_of_nonpos, iff_of_false, Real.sqrt_pos, Eq.trans_lt, LT.lt.not_ge, LE.le.trans_lt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 < x
hy : y ≤ 0
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
exact iff_of_false ((sqrt_eq_zero_of_nonpos hy).trans_lt <| sqrt_pos.2 hx).not_ge
      (hy.trans_lt hx).not_ge

Premises used: Iff.mpr, Real.sqrt_eq_zero_of_nonpos, iff_of_false, Real.sqrt_pos, Eq.trans_lt, LT.lt.not_ge, LE.le.trans_lt
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
sqrt_le_sqrt_iff hy

Premises used: Real.sqrt_le_sqrt_iff
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x y : ℝ
hx : 0 < x
hy : 0 ≤ y
⊢ √x ≤ √y ↔ x ≤ y

Tactic:
exact sqrt_le_sqrt_iff hy

Premises used: Real.sqrt_le_sqrt_iff
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : √1 ≤ √x ↔ √1 ≤ x
rw₁ : 1 ≤ x ↔ √1 ≤ x
rw₂ rw₃ : 1 ≤ x ↔ 1 ≤ x
⊢ 1 ≤ √x ↔ 1 ≤ x

Tactic:
rw [← sqrt_one, sqrt_le_sqrt_iff' zero_lt_one, sqrt_one]

Premises used: zero_lt_one, Real.sqrt_one, Real.sqrt_le_sqrt_iff'
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
rw : √x ≤ √1 ↔ x ≤ √1
rw₁ : x ≤ 1 ↔ x ≤ √1
rw₂ rw₃ : x ≤ 1 ↔ x ≤ 1
⊢ √x ≤ 1 ↔ x ≤ 1

Tactic:
rw [← sqrt_one, sqrt_le_sqrt_iff zero_le_one, sqrt_one]

Premises used: Real.sqrt_le_sqrt_iff, zero_le_one, Real.sqrt_one
-- Module: Mathlib.Data.Real.Sqrt
Goal:
x : ℝ
⊢ IsSquare x ↔ 0 ≤ x

Tactic:
⟨(·.nonneg), (⟨√x, mul_self_sqrt · |>.symm⟩)⟩

Premises used: Real.mul_self_sqrt, Iff.intro, Exists.intro, Real.sqrt, IsSquare.nonneg, Eq.symm
-- Module: Mathlib.Data.Real.Sqrt
Goal:
rw : √1 < √2
⊢ 1 < √2

Tactic:
rw [← Real.sqrt_one]

Premises used: Real.sqrt_one
-- Module: Mathlib.Data.Real.Sqrt
Goal:
h : LT.lt (α := ℝ) 1 2
⊢ √1 < √2

Tactic:
gcongr
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ LT.lt (α := ℝ) 1 2

Tactic:
simp
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ 0 ≤ √2

Tactic:
positivity
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ 0 ≤ 3 / 2

Tactic:
positivity
-- Module: Mathlib.Data.Real.Sqrt
Goal:
rw : HPow.hPow (β := ℕ) (√2) 2 < HPow.hPow (β := ℕ) (3 / 2) 2
⊢ √2 < 3 / 2

Tactic:
rw [← sq_lt_sq₀ (by positivity) (by positivity)]

Premises used: sq_lt_sq₀
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ HPow.hPow (β := ℕ) (√2) 2 < HPow.hPow (β := ℕ) (3 / 2) 2

Tactic:
grind
-- Module: Mathlib.Data.Real.Sqrt
Goal:
⊢ (√2 - 1)⁻¹ = √2 + 1

Tactic:
grind