-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
⊢ ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2)
        (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.1 n.2 - f n.1.1 x) +
          HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.2 n.2 - f n.1.2 x)) <
      ε
have obtain : ∀ (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),
  ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2)
        (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.1 n.2 - f n.1.1 x) +
          HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.2 n.2 - f n.1.2 x)) <
      ε
Tactic: obtain ⟨a, b, c, d, e⟩ := eventually_prod_iff.1 (hfg'.and this)