x : ℝ
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
x : ℝ
⊢ (deriv^[2]) (fun x => sqrt x * log x) x = -log x / (↑4 * sqrt x ^ 3)
simp only [Nat.iterate, deriv_sqrt_mul_log']
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)

case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
x : ℝ
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
cases' le_or_lt x 0 with hx hx
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = 0
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
rw [sqrt_eq_zero_of_nonpos hx, zero_pow zero_lt_three, MulZeroClass.mul_zero, div_zero]
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => (2 + log x) / (2 * sqrt x)) 0 (Iic 0) x
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = 0
refine' HasDerivWithinAt.deriv_eq_zero _ (uniqueDiffOn_Iic 0 x hx)
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * sqrt x) = 0
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => (2 + log x) / (2 * sqrt x)) 0 (Iic 0) x
refine' (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => _) hx
no goals
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * sqrt x) = 0
rw [sqrt_eq_zero_of_nonpos hx, MulZeroClass.mul_zero, div_zero]
case inr
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
have h₀ : sqrt x ≠ 0 := sqrt_ne_zero'.2 hx
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) = (x⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
case inr
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ deriv (fun x => (2 + log x) / (2 * sqrt x)) x = -log x / (↑4 * sqrt x ^ 3)
convert (((hasDerivAt_log hx.ne').const_add 2).div ((hasDerivAt_sqrt hx.ne').const_mul 2) <|
  mul_ne_zero two_ne_zero h₀).deriv using 1
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) =
    ((sqrt x * sqrt x)⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) = (x⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
nth_rw 3 [← mul_self_sqrt hx.le]
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -(log x * (sqrt x * sqrt x * (2 * sqrt x) * (2 * sqrt x) ^ 2)) =
    (2 * sqrt x * (2 * sqrt x) - sqrt x * sqrt x * ((2 + log x) * 2)) * (4 * sqrt x ^ 3)
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -log x / (↑4 * sqrt x ^ 3) =
    ((sqrt x * sqrt x)⁻¹ * (2 * sqrt x) - (2 + log x) * (2 * (1 / (2 * sqrt x)))) / (2 * sqrt x) ^ 2
field_simp
no goals
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : sqrt x ≠ 0
⊢ -(log x * (sqrt x * sqrt x * (2 * sqrt x) * (2 * sqrt x) ^ 2)) =
    (2 * sqrt x * (2 * sqrt x) - sqrt x * sqrt x * ((2 + log x) * 2)) * (4 * sqrt x ^ 3)
ring