case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -sqrt y ≤ x ∧ x ≤ sqrt y

case mpr
x y : ℝ
h : 0 ≤ y
⊢ -sqrt y ≤ x ∧ x ≤ sqrt y → x ^ 2 ≤ y
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y ↔ -sqrt y ≤ x ∧ x ≤ sqrt y
constructor
no goals
case mp
x y : ℝ
h : 0 ≤ y
⊢ x ^ 2 ≤ y → -sqrt y ≤ x ∧ x ≤ sqrt y
simpa only [abs_le] using abs_le_sqrt
case mpr
x y : ℝ
h : 0 ≤ y
⊢ abs x ≤ sqrt y → abs x ^ 2 ≤ y
case mpr
x y : ℝ
h : 0 ≤ y
⊢ -sqrt y ≤ x ∧ x ≤ sqrt y → x ^ 2 ≤ y
rw [← abs_le, ← sq_abs]
no goals
case mpr
x y : ℝ
h : 0 ≤ y
⊢ abs x ≤ sqrt y → abs x ^ 2 ≤ y
exact (le_sqrt (abs_nonneg x) h).mp