<VAR>ι : Type u_1<VAR>l : Filter ι<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>𝕜 : Type u_3<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ι → E → G<VAR>g : E → G<VAR>f' : ι → E → E →L[𝕜] G<VAR>g' : E → E →L[𝕜] G<VAR>x : E<VAR>hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)<VAR>hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2<VAR>hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))<VAR>A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E<VAR>hl : l ≠ ⊥<VAR>this✝ : l.NeBot<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>q : ℚ<VAR>hqpos : 0 < q<VAR>hqε : ↑q < ε<VAR>hfg' : ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ↑q<VAR>this : ∀ᶠ (x : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1) (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧ HasFDerivAt (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1) (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1 (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2<VAR>a : ι × ι → Prop<VAR>b : ∀ᶠ (x : ι × ι) in l ×ˢ l, a x<VAR>c : E → Prop<VAR>d : ∀ᶠ (y : E) in 𝓝 x, c y<VAR>e : ∀ {x : ι × ι}, a x → ∀ {y : E}, c y → dist (0 (x, y).2) (f' (x, y).1.1 (x, y).2 - f' (x, y).1.2 (x, y).2) < ↑q ∧ HasFDerivAt (f ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).1.1) (f' ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).1.1 ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).1.2) ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).1.2 ∧ HasFDerivAt (f ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).2.1) (f' ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).2.1 ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).2.2) ((((x, y).1, (x, y).2, (x, y).2).1.1, ((x, y).1, (x, y).2, (x, y).2).2.1), ((x, y).1, (x, y).2, (x, y).2).1.2, ((x, y).1, (x, y).2, (x, y).2).2.2).2.2<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hr' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x r → c x_1<VAR>n : ι × ι<VAR>hn : a n<VAR>y : E<VAR>hy : (fun e => Metric.ball x r e) y<VAR>hyz' : ¬x = y<VAR>hyz : 0 < ‖y - x‖<GOAL>‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ ≤ ↑q * ‖y - x‖