[GOAL]
x y : ℝ≥0
⊢ 0 ^ 2 = x ↔ x = 0
[PROOFSTEP]
rw [eq_comm, sq, zero_mul]
[GOAL]
x✝ y x : ℝ≥0
⊢ ↑sqrt x * ↑sqrt x = x
[PROOFSTEP]
rw [← sq, sq_sqrt]
[GOAL]
x✝ y x : ℝ≥0
⊢ ↑sqrt (x * x) = x
[PROOFSTEP]
rw [← sq, sqrt_sq x]
[GOAL]
x✝ y✝ x y : ℝ≥0
⊢ ↑sqrt (x * y) = ↑sqrt x * ↑sqrt y
[PROOFSTEP]
rw [sqrt_eq_iff_sq_eq, mul_pow, sq_sqrt, sq_sqrt]
[GOAL]
x y : ℝ≥0
⊢ 0 < ↑sqrt x ↔ 0 < x
[PROOFSTEP]
simp [pos_iff_ne_zero]
[GOAL]
f : CauSeq ℚ abs
⊢ 0 ≤ sqrtAux f 0
[PROOFSTEP]
rw [sqrtAux, Rat.mkRat_eq, Rat.divInt_eq_div]
[GOAL]
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (Int.toNat (↑f 0).num)) / ↑↑(Nat.sqrt (↑f 0).den)
[PROOFSTEP]
apply div_nonneg
[GOAL]
case ha
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (Int.toNat (↑f 0).num))
[PROOFSTEP]
exact Int.cast_nonneg.2 (Int.ofNat_nonneg _)
[GOAL]
case hb
f : CauSeq ℚ abs
⊢ 0 ≤ ↑↑(Nat.sqrt (↑f 0).den)
[PROOFSTEP]
exact Int.cast_nonneg.2 (Int.ofNat_nonneg _)
[GOAL]
x✝ y : ℝ
x : ℝ≥0
⊢ ↑(↑NNReal.sqrt x) = sqrt ↑x
[PROOFSTEP]
rw [Real.sqrt, Real.toNNReal_coe]
[GOAL]
x y : ℝ
h : x ≤ 0
⊢ sqrt x = 0
[PROOFSTEP]
simp [sqrt, Real.toNNReal_eq_zero.2 h]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x * sqrt x = x
[PROOFSTEP]
rw [sqrt, ← NNReal.coe_mul, NNReal.mul_self_sqrt, Real.coe_toNNReal _ h]
[GOAL]
x y : ℝ
⊢ sqrt x = y ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : ℝ
⊢ sqrt x = y → y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
x : ℝ
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
[PROOFSTEP]
cases' le_or_lt 0 x with hle hlt
[GOAL]
case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
[PROOFSTEP]
exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩
[GOAL]
case mp.inr
x : ℝ
hlt : x < 0
⊢ sqrt x * sqrt x = x ∧ 0 ≤ sqrt x ∨ x < 0 ∧ sqrt x = 0
[PROOFSTEP]
exact Or.inr ⟨hlt, sqrt_eq_zero_of_nonpos hlt.le⟩
[GOAL]
case mpr
x y : ℝ
⊢ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 → sqrt x = y
[PROOFSTEP]
rintro (⟨rfl, hy⟩ | ⟨hx, rfl⟩)
[GOAL]
case mpr.inl.intro
y : ℝ
hy : 0 ≤ y
⊢ sqrt (y * y) = y
case mpr.inr.intro x : ℝ hx : x < 0 ⊢ sqrt x = 0
[PROOFSTEP]
exacts [sqrt_mul_self hy, sqrt_eq_zero_of_nonpos hx.le]
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : sqrt x = y
⊢ y * y = x
[PROOFSTEP]
rw [← h, mul_self_sqrt hx]
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : y * y = x
⊢ sqrt x = y
[PROOFSTEP]
rw [← h, sqrt_mul_self hy]
[GOAL]
x y : ℝ
h : 0 < y
⊢ sqrt x = y ↔ y * y = x
[PROOFSTEP]
simp [sqrt_eq_cases, h.ne', h.le]
[GOAL]
x y : ℝ
⊢ 1 * 1 = x ↔ x = 1
[PROOFSTEP]
rw [eq_comm, mul_one]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x ^ 2 = x
[PROOFSTEP]
rw [sq, mul_self_sqrt h]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt (x ^ 2) = x
[PROOFSTEP]
rw [sq, sqrt_mul_self h]
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ sqrt x = y ↔ y ^ 2 = x
[PROOFSTEP]
rw [sq, sqrt_eq_iff_mul_self_eq hx hy]
[GOAL]
x✝ y x : ℝ
⊢ sqrt (x * x) = |x|
[PROOFSTEP]
rw [← abs_mul_abs_self x, sqrt_mul_self (abs_nonneg _)]
[GOAL]
x✝ y x : ℝ
⊢ sqrt (x ^ 2) = |x|
[PROOFSTEP]
rw [sq, sqrt_mul_self_eq_abs]
[GOAL]
x y : ℝ
⊢ sqrt 0 = 0
[PROOFSTEP]
simp [sqrt]
[GOAL]
x y : ℝ
⊢ sqrt 1 = 1
[PROOFSTEP]
simp [sqrt]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt x ≤ sqrt y ↔ x ≤ y
[PROOFSTEP]
rw [sqrt, sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt_iff, Real.toNNReal_le_toNNReal_iff hy]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ sqrt x < sqrt y ↔ x < y
[PROOFSTEP]
rw [sqrt, sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt_iff, toNNReal_lt_toNNReal_iff hy]
[GOAL]
x y : ℝ
h : x ≤ y
⊢ sqrt x ≤ sqrt y
[PROOFSTEP]
rw [sqrt, sqrt, NNReal.coe_le_coe, NNReal.sqrt_le_sqrt_iff]
[GOAL]
x y : ℝ
h : x ≤ y
⊢ toNNReal x ≤ toNNReal y
[PROOFSTEP]
exact toNNReal_le_toNNReal h
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt x ≤ y ↔ x ≤ y ^ 2
[PROOFSTEP]
rw [sqrt, ← Real.le_toNNReal_iff_coe_le hy, NNReal.sqrt_le_iff, sq, ← Real.toNNReal_mul hy,
  Real.toNNReal_le_toNNReal_iff (mul_self_nonneg y), sq]
[GOAL]
x y : ℝ
⊢ sqrt x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
[PROOFSTEP]
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]
[GOAL]
x y : ℝ
⊢ 0 ≤ y → (sqrt x ≤ y ↔ x ≤ y ^ 2)
[PROOFSTEP]
exact sqrt_le_left
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ sqrt x < y ↔ x < y ^ 2
[PROOFSTEP]
rw [← sqrt_lt_sqrt_iff hx, sqrt_sq hy]
[GOAL]
x y : ℝ
hy : 0 < y
⊢ sqrt x < y ↔ x < y ^ 2
[PROOFSTEP]
rw [← sqrt_lt_sqrt_iff_of_pos (pow_pos hy _), sqrt_sq hy.le]
[GOAL]
x y : ℝ
h : x ^ 2 ≤ y
⊢ |x| ≤ sqrt y
[PROOFSTEP]
rw [← sqrt_sq_eq_abs]
[GOAL]
x y : ℝ
h : x ^ 2 ≤ y
⊢ sqrt (x ^ 2) ≤ sqrt y
[PROOFSTEP]
exact sqrt_le_sqrt h
[GOAL]
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y ↔ -sqrt y ≤ x ∧ x ≤ sqrt y
[PROOFSTEP]
constructor
[GOAL]
case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -sqrt y ≤ x ∧ x ≤ sqrt y
[PROOFSTEP]
simpa only [abs_le] using abs_le_sqrt
[GOAL]
case mpr
x y : ℝ
h : 0 ≤ y
⊢ -sqrt y ≤ x ∧ x ≤ sqrt y → x ^ 2 ≤ y
[PROOFSTEP]
rw [← abs_le, ← sq_abs]
[GOAL]
case mpr
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ sqrt y → |x| ^ 2 ≤ y
[PROOFSTEP]
exact (le_sqrt (abs_nonneg x) h).mp
[GOAL]
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ sqrt x = sqrt y ↔ x = y
[PROOFSTEP]
simp [le_antisymm_iff, hx, hy]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x = 0 ↔ x = 0
[PROOFSTEP]
simpa using sqrt_inj h le_rfl
[GOAL]
x y : ℝ
⊢ sqrt x = 0 ↔ x ≤ 0
[PROOFSTEP]
rw [sqrt, NNReal.coe_eq_zero, NNReal.sqrt_eq_zero, Real.toNNReal_eq_zero]
[GOAL]
x y : ℝ
h : 0 ≤ x
⊢ sqrt x ≠ 0 ↔ x ≠ 0
[PROOFSTEP]
rw [not_iff_not, sqrt_eq_zero h]
[GOAL]
x y : ℝ
⊢ sqrt x ≠ 0 ↔ 0 < x
[PROOFSTEP]
rw [← not_le, not_iff_not, sqrt_eq_zero']
[GOAL]
x y : ℝ
⊢ sqrt x ≤ 0 ↔ sqrt x = 0
[PROOFSTEP]
simp [le_antisymm_iff, sqrt_nonneg]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ sqrt (x * y) = sqrt x * sqrt y
[PROOFSTEP]
simp_rw [sqrt, ← NNReal.coe_mul, NNReal.coe_eq, Real.toNNReal_mul hx, NNReal.sqrt_mul]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt (x * y) = sqrt x * sqrt y
[PROOFSTEP]
rw [mul_comm, sqrt_mul hy, mul_comm]
[GOAL]
x : ℝ
⊢ sqrt x⁻¹ = (sqrt x)⁻¹
[PROOFSTEP]
rw [sqrt, Real.toNNReal_inv, NNReal.sqrt_inv, NNReal.coe_inv, sqrt]
[GOAL]
x : ℝ
hx : 0 ≤ x
y : ℝ
⊢ sqrt (x / y) = sqrt x / sqrt y
[PROOFSTEP]
rw [division_def, sqrt_mul hx, sqrt_inv, division_def]
[GOAL]
x y : ℝ
hy : 0 ≤ y
⊢ sqrt (x / y) = sqrt x / sqrt y
[PROOFSTEP]
rw [division_def, sqrt_mul' x (inv_nonneg.2 hy), sqrt_inv, division_def]
[GOAL]
x : ℝ
⊢ x / sqrt x = sqrt x
[PROOFSTEP]
cases' le_or_lt x 0 with h h
[GOAL]
case inl
x : ℝ
h : x ≤ 0
⊢ x / sqrt x = sqrt x
[PROOFSTEP]
rw [sqrt_eq_zero'.mpr h, div_zero]
[GOAL]
case inr
x : ℝ
h : 0 < x
⊢ x / sqrt x = sqrt x
[PROOFSTEP]
rw [div_eq_iff (sqrt_ne_zero'.mpr h), mul_self_sqrt h.le]
[GOAL]
x : ℝ
⊢ sqrt x / x = 1 / sqrt x
[PROOFSTEP]
rw [← div_sqrt, one_div_div, div_sqrt]
[GOAL]
x : ℝ
⊢ sqrt x / x = (sqrt x)⁻¹
[PROOFSTEP]
rw [sqrt_div_self', one_div]
[GOAL]
x y : ℝ
hx : 0 ≤ x
⊢ x < sqrt y ↔ x ^ 2 < y
[PROOFSTEP]
rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]
[GOAL]
x y : ℝ
⊢ x ^ 2 < y ↔ -sqrt y < x ∧ x < sqrt y
[PROOFSTEP]
rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]
[GOAL]
x y : ℝ
h : sqrt x < y
⊢ x < y ^ 2
[PROOFSTEP]
have hy := x.sqrt_nonneg.trans_lt h
[GOAL]
x y : ℝ
h : sqrt x < y
hy : 0 < y
⊢ x < y ^ 2
[PROOFSTEP]
rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]
[GOAL]
a : ℕ
⊢ ↑(Nat.sqrt a) ≤ sqrt ↑a
[PROOFSTEP]
rw [Real.le_sqrt (Nat.cast_nonneg _) (Nat.cast_nonneg _)]
[GOAL]
a : ℕ
⊢ ↑(Nat.sqrt a) ^ 2 ≤ ↑a
[PROOFSTEP]
norm_cast
[GOAL]
a : ℕ
⊢ Nat.sqrt a ^ 2 ≤ a
[PROOFSTEP]
exact Nat.sqrt_le' a
[GOAL]
a : ℕ
⊢ sqrt ↑a ≤ ↑(Nat.sqrt a) + 1
[PROOFSTEP]
rw [Real.sqrt_le_iff]
[GOAL]
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1 ∧ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
[PROOFSTEP]
constructor
[GOAL]
case left
a : ℕ
⊢ 0 ≤ ↑(Nat.sqrt a) + 1
[PROOFSTEP]
norm_cast
[GOAL]
case left
a : ℕ
⊢ 0 ≤ Nat.sqrt a + 1
[PROOFSTEP]
apply zero_le
[GOAL]
case right
a : ℕ
⊢ ↑a ≤ (↑(Nat.sqrt a) + 1) ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
case right
a : ℕ
⊢ a ≤ (Nat.sqrt a + 1) ^ 2
[PROOFSTEP]
exact le_of_lt (Nat.lt_succ_sqrt' a)
[GOAL]
r : ℝ
⊢ 0 ≤ r ↔ ∃ s, r = star s * s
[PROOFSTEP]
refine ⟨fun hr => ⟨sqrt r, (mul_self_sqrt hr).symm⟩, ?_⟩
[GOAL]
r : ℝ
⊢ (∃ s, r = star s * s) → 0 ≤ r
[PROOFSTEP]
rintro ⟨s, rfl⟩
[GOAL]
case intro
s : ℝ
⊢ 0 ≤ star s * s
[PROOFSTEP]
exact mul_self_nonneg s
