∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') s x