∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : ι → 𝕜 → G} {g g' : 𝕜 → G} {x : 𝕜}
  [IsRCLikeNormedField 𝕜] [l.NeBot] {s : Set 𝕜},
  IsOpen s →
    TendstoLocallyUniformlyOn (deriv ∘ f) g' l s →
      (∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s) →
        (∀ x ∈ s, Filter.Tendsto (fun n => f n x) l (nhds (g x))) → x ∈ s → HasDerivAt g (g' x) x