case inl
x : ℝ
h : x ≤ 0
⊢ x / sqrt x = sqrt x

case inr
x : ℝ
h : 0 < x
⊢ x / sqrt x = sqrt x
x : ℝ
⊢ x / sqrt x = sqrt x
cases' le_or_lt x 0 with h h
no goals
case inl
x : ℝ
h : x ≤ 0
⊢ x / sqrt x = sqrt x
rw [sqrt_eq_zero'.mpr h, div_zero]
no goals
case inr
x : ℝ
h : 0 < x
⊢ x / sqrt x = sqrt x
rw [div_eq_iff (sqrt_ne_zero'.mpr h), mul_self_sqrt h.le]