-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : (↑q : ℝ) < ε
hfg' : ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < (↑q : ℝ)
this :
  ∀ᶠ (x : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (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.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (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
a : ι × ι → Prop
b : ∀ᶠ (x : ι × ι) in l ×ˢ l, a x
c : E → Prop
d : ∀ᶠ (y : E) in 𝓝 x, c y
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.{u_6, u_5, u_7} (𝕜 := 𝕜)
                (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.{u_6, u_5, u_7} (𝕜 := 𝕜)
                (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
r : ℝ
hr : 0 < r
hr' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x r → c x_1
⊢ ∃ (pa : ι × ι → Prop),
    (∀ᶠ (x : ι × ι) in l ×ˢ l, pa x) ∧
      ∃ (pb : E → Prop),
        (∀ᶠ (y : E) in 𝓝 x, pb y) ∧
          ∀ {x_1 : ι × ι},
            pa x_1 →
              ∀ {y : E},
                pb y →
                  dist (0 (x_1, y).2)
                      (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖(x_1, y).2 - x‖ : 𝕜)⁻¹
                            (f (x_1, y).1.1 (x_1, y).2 - f (x_1, y).1.1 x) +
                        HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖(x_1, y).2 - x‖ : 𝕜)⁻¹
                          (f (x_1, y).1.2 (x_1, y).2 - f (x_1, y).1.2 x)) <
                    ε

Tactic:
⟨_, b, fun e : E => Metric.ball x r e,
      eventually_mem_set.mpr (Metric.nhds_basis_ball.mem_of_mem hr), fun {n} hn {y} hy => ?_⟩

Premises used: Iff.mpr, Metric.ball, And.intro, Exists.intro, Metric.nhds_basis_ball, Filter.HasBasis.mem_of_mem, Filter.eventually_mem_set