x y : ℝ
h : sqrt x < y
hy : 0 < y
⊢ x < y ^ 2
x y : ℝ
h : sqrt x < y
⊢ x < y ^ 2
have hy := x.sqrt_nonneg.trans_lt h
no goals
x y : ℝ
h : sqrt x < y
hy : 0 < y
⊢ x < y ^ 2
rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]