case inl
x : ℝ
hx : 0 < x
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)

case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
x : ℝ
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
cases' lt_or_le 0 x with hx hx
no goals
case inl
x : ℝ
hx : 0 < x
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
exact (hasDerivAt_sqrt_mul_log hx.ne').deriv
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = 0
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = (2 + log x) / (2 * sqrt x)
rw [sqrt_eq_zero_of_nonpos hx, MulZeroClass.mul_zero, div_zero]
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => sqrt x * log x) 0 (Iic 0) x
case inr
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => sqrt x * log x) x = 0
refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
case inr
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ sqrt x * log x = 0
case inr
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => sqrt x * log x) 0 (Iic 0) x
refine' (hasDerivWithinAt_const x _ 0).congr_of_mem (fun x hx => _) hx
no goals
case inr
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ sqrt x * log x = 0
rw [sqrt_eq_zero_of_nonpos hx, MulZeroClass.zero_mul]