-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
this :
  ∀ᶠ (x : Prod.{u_1, u_2} (ι × ι) 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
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) < ε ∧
            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
R : ℝ
hR : 0 < R
hR' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x R → c x_1
r : ℝ := min 1 R
hr : 0 < r
hr' : ∀ ⦃y : E⦄, y ∈ Metric.ball x r → c y
hxy : ∀ y ∈ Metric.ball x r, ‖y - x‖ < 1
hxyε : ∀ y ∈ Metric.ball x r, ε * ‖y - x‖ < ε
left :
  ∀ {n : ι × ι} (hn : a n) {y : E} (hy : (fun (e : E) ↦ Metric.ball x r e) y),
    dist (0 (n, y).2) (f (n, y).1.1 (n, y).2 - f (n, y).1.2 (n, y).2 - (f (n, y).1.1 x - f (n, y).1.2 x)) < ε
⊢ ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2) (f n.1.1 n.2 - f n.1.2 n.2 - (f n.1.1 x - f n.1.2 x)) < ε

Tactic:
refine
      eventually_prod_iff.mpr
        ⟨_, 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, Filter.eventually_prod_iff, And.intro, Exists.intro, Metric.nhds_basis_ball, Filter.HasBasis.mem_of_mem, Filter.eventually_mem_set