-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem hasFDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
    (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
    (hf : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : ∀ᶠ y in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) : HasFDerivAt g (g' x) x

Proof state:
case refine_1
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a =>
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x), dist ((↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε

Tactic:
apply ((this ε hε).filter_mono curry_le_prod).mono

Result:
case refine_1
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a =>
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist ((↑‖n.2 - x‖)⁻¹ • (g n.2 - g x)) ((↑‖n.2 - x‖)⁻¹ • (f n.1 n.2 - f n.1 x)) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ (x_1 : ι × E),
    dist ((↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x)) ((↑‖x_1.2 - x‖)⁻¹ • (f x_1.1 x_1.2 - f x_1.1 x)) < ε →
      dist ((↑‖x_1.2 - x‖)⁻¹ • (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε

Proof state:
case refine_2
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a =>
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist (‖x_1 - (n, x).2‖⁻¹ * ‖f (n, x).1 x_1 - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (x_1 - (n, x).2)‖) 0 < ε
y : E
hy : dist (‖y - (n, x).2‖⁻¹ * ‖f (n, x).1 y - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (y - (n, x).2)‖) 0 < ε
⊢ dist ((↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x))) 0 <
    ε

Tactic:
rw [dist_eq_norm] at hy ⊢

Result:
case refine_2
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a => (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a =>
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a => (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist (‖x_1 - (n, x).2‖⁻¹ * ‖f (n, x).1 x_1 - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (x_1 - (n, x).2)‖) 0 < ε
y : E
hy : ‖‖y - (n, x).2‖⁻¹ * ‖f (n, x).1 y - f (n, x).1 (n, x).2 - (f' (n, x).1 (n, x).2) (y - (n, x).2)‖ - 0‖ < ε
⊢ ‖(↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x)) - 0‖ < ε