∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x