x y : ℝ
⊢ 0 ≤ y → (sqrt x ≤ y ↔ x ≤ y ^ 2)
x y : ℝ
⊢ sqrt x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2
rw [← and_iff_right_of_imp fun h => (sqrt_nonneg x).trans h, and_congr_right_iff]
no goals
x y : ℝ
⊢ 0 ≤ y → (sqrt x ≤ y ↔ x ≤ y ^ 2)
exact sqrt_le_left