case h.e'_7
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * sqrt x) = 1 / (2 * sqrt x) * log x + sqrt x * x⁻¹
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun x => sqrt x * log x) ((2 + log x) / (2 * sqrt x)) x
convert (hasDerivAt_sqrt hx).mul (hasDerivAt_log hx) using 1
no goals
case h.e'_7
x : ℝ
hx : x ≠ 0
⊢ (2 + log x) / (2 * sqrt x) = 1 / (2 * sqrt x) * log x + sqrt x * x⁻¹
rw [add_div, div_mul_right (sqrt x) two_ne_zero, ← div_eq_mul_inv, sqrt_div_self', add_comm,
  div_eq_mul_one_div, mul_comm]