no goals
f g : ℂ → ℂ
s : Set ℂ
f' g' x c : ℂ
⊢ ↑((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' +
          (f x ^ g x * log (f x)) • ContinuousLinearMap.smulRight 1 g')
      1 =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'
simp only [Algebra.id.smul_eq_mul, one_mul, ContinuousLinearMap.one_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.add_apply, Pi.smul_apply,
  ContinuousLinearMap.coe_smul']