∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} [CompleteSpace 𝕜] [CharZero 𝕜] {E : Type u_2}
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {g : 𝕜 → E},
  AnalyticAt 𝕜 f x → deriv f x ≠ 0 → (AnalyticAt 𝕜 (g ∘ f) x ↔ AnalyticAt 𝕜 g (f x))