case h.e'_7
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) =
    ↑((((fun x => (f x, g x)) x).snd * ((fun x => (f x, g x)) x).fst ^ (((fun x => (f x, g x)) x).snd - 1)) •
            ContinuousLinearMap.fst ℝ ℝ ℝ +
          (((fun x => (f x, g x)) x).fst ^ ((fun x => (f x, g x)) x).snd * log ((fun x => (f x, g x)) x).fst) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (f', g')
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x
convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x
  (hf.prod hg) using 1
no goals
case h.e'_7
x y z : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x) =
    ↑((((fun x => (f x, g x)) x).snd * ((fun x => (f x, g x)) x).fst ^ (((fun x => (f x, g x)) x).snd - 1)) •
            ContinuousLinearMap.fst ℝ ℝ ℝ +
          (((fun x => (f x, g x)) x).fst ^ ((fun x => (f x, g x)) x).snd * log ((fun x => (f x, g x)) x).fst) •
            ContinuousLinearMap.snd ℝ ℝ ℝ)
      (f', g')
simp [mul_assoc, mul_comm, mul_left_comm]