-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem deriv2_sqrt_mul_log (x : ℝ) :
    deriv^[2] (fun x => √x * log x) x = -log x / (4 * √x ^ 3)

Proof state:
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, zero_pow three_ne_zero, mul_zero, div_zero]

Result:
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = 0

Proof state:
case h.e'_3
x : ℝ
hx : 0 < x
sqx : ℝ
h₀ : sqx ≠ 0
⊢ -log x / (4 * sqx ^ 3) = ((sqx * sqx)⁻¹ * (2 * sqx) - (2 + log x) * (2 * (1 / (2 * sqx)))) / (2 * sqx) ^ 2

Tactic:
field_simp

Result:
case h.e'_3
x : ℝ
hx : 0 < x
sqx : ℝ
h₀ : sqx ≠ 0
⊢ -(log x * (sqx * sqx * (2 * sqx) * (2 * sqx) ^ 2)) =
    (2 * sqx * (2 * sqx) - sqx * sqx * ((2 + log x) * 2)) * (4 * sqx ^ 3)

Proof state:
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => (2 + log x) / (2 * √x)) 0 (Iic 0) x

Tactic:
refine (hasDerivWithinAt_const _ _ 0).congr_of_mem (fun x hx => ?_) hx

Result:
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * √x) = 0

Proof state:
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = 0

Tactic:
refine HasDerivWithinAt.deriv_eq_zero ?_ (uniqueDiffOn_Iic 0 x hx)

Result:
case inl
x : ℝ
hx : x ≤ 0
⊢ HasDerivWithinAt (fun x => (2 + log x) / (2 * √x)) 0 (Iic 0) x

Proof state:
case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Tactic:
have h₀ : √x ≠ 0 := sqrt_ne_zero'.2 hx

Result:
case inr
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Proof state:
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ -log x / (4 * √x ^ 3) = ((√x * √x)⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / (2 * √x) ^ 2

Tactic:
generalize √x = sqx at h₀

Result:
case h.e'_3
x : ℝ
hx : 0 < x
sqx : ℝ
h₀ : sqx ≠ 0
⊢ -log x / (4 * sqx ^ 3) = ((sqx * sqx)⁻¹ * (2 * sqx) - (2 + log x) * (2 * (1 / (2 * sqx)))) / (2 * sqx) ^ 2

Proof state:
case h.e'_3
x : ℝ
hx : 0 < x
sqx : ℝ
h₀ : sqx ≠ 0
⊢ -(log x * (sqx * sqx * (2 * sqx) * (2 * sqx) ^ 2)) =
    (2 * sqx * (2 * sqx) - sqx * sqx * ((2 + log x) * 2)) * (4 * sqx ^ 3)

Tactic:
ring

Result:
no goals

Proof state:
case inr
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Tactic:
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

Result:
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ -log x / (4 * √x ^ 3) = (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / (2 * √x) ^ 2

Proof state:
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ -log x / (4 * √x ^ 3) = (x⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / (2 * √x) ^ 2

Tactic:
nth_rw 3 [← mul_self_sqrt hx.le]

Result:
case h.e'_3
x : ℝ
hx : 0 < x
h₀ : √x ≠ 0
⊢ -log x / (4 * √x ^ 3) = ((√x * √x)⁻¹ * (2 * √x) - (2 + log x) * (2 * (1 / (2 * √x)))) / (2 * √x) ^ 2

Proof state:
case inl
x✝ : ℝ
hx✝ : x✝ ≤ 0
x : ℝ
hx : x ∈ Iic 0
⊢ (2 + log x) / (2 * √x) = 0

Tactic:
rw [sqrt_eq_zero_of_nonpos hx, mul_zero, div_zero]

Result:
no goals

Proof state:
x : ℝ
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Tactic:
rcases le_or_lt x 0 with hx | hx

Result:
case inl
x : ℝ
hx : x ≤ 0
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

case inr
x : ℝ
hx : 0 < x
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)

Proof state:
x : ℝ
⊢ deriv^[2] (fun x => √x * log x) x = -log x / (4 * √x ^ 3)

Tactic:
simp only [Nat.iterate, deriv_sqrt_mul_log']

Result:
x : ℝ
⊢ deriv (fun x => (2 + log x) / (2 * √x)) x = -log x / (4 * √x ^ 3)