-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem difference_quotients_converge_uniformly
    {E : Type*} [NormedAddCommGroup E] {𝕜 : Type*} [RCLike 𝕜]
    [NormedSpace 𝕜 E] {G : Type*} [NormedAddCommGroup G] [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 (f n.1) (f' n.1 n.2) n.2)
    (hfg : ∀ᶠ y : E in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) :
    TendstoUniformlyOnFilter (fun n : ι => fun y : E => (‖y - x‖⁻¹ : 𝕜) • (f n y - f n x))
      (fun y : E => (‖y - x‖⁻¹ : 𝕜) • (g y - g x)) l (𝓝 x)

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 (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
hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
obtain ⟨q, hqpos, hqε⟩ := exists_pos_rat_lt hε

Result:
case intro.intro
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 (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
hfg' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : ↑q < ε
⊢ ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2) ((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x) - (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Proof state:
case pos
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 (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 : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f' n.1.1 n.2 - f' n.1.2 n.2) < ↑q
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
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
                (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
n : ι × ι
hn : a n
y : E
hy : (fun e => Metric.ball x r e) y
hyz' : x = y
⊢ ‖y - x‖⁻¹ * ‖f n.1 y - f n.1 x - (f n.2 y - f n.2 x)‖ ≤ ↑q

Tactic:
simp [hyz', hqpos.le]

Result:
no goals