-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem hasDerivAt_of_tendstoUniformlyOnFilter [NeBot l]
    (hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x))
    (hf : ∀ᶠ n : ι × 𝕜 in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2)
    (hfg : ∀ᶠ y in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))) : HasDerivAt g (g' x) x

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.2) (f' n.1 n.2) < q
⊢ dist (G' n.2) (F' n.1 n.2) < ε

Tactic:
refine lt_of_le_of_lt ?_ hq'

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.2) (f' n.1 n.2) < q
⊢ dist (G' n.2) (F' n.1 n.2) ≤ q

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.2 - f' n.1 n.2‖ < q
z : 𝕜
⊢ ‖z • g' n.2 - z • f' n.1 n.2‖ ≤ q * ‖z‖

Tactic:
rw [← smul_sub, norm_smul, mul_comm]

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.2 - f' n.1 n.2‖ < q
z : 𝕜
⊢ ‖g' n.2 - f' n.1 n.2‖ * ‖z‖ ≤ q * ‖z‖

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : dist (g' n.2) (f' n.1 n.2) < q
⊢ dist (G' n.2) (F' n.1 n.2) ≤ q

Tactic:
simp only [dist_eq_norm] at hn ⊢

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.2 - f' n.1 n.2‖ < q
⊢ ‖G' n.2 - F' n.1 n.2‖ ≤ q

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.2 - f' n.1 n.2‖ < q
z : 𝕜
⊢ ‖(G' n.2 - F' n.1 n.2) z‖ ≤ q * ‖z‖

Tactic:
simp only [F', G', ContinuousLinearMap.coe_sub', Pi.sub_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply]

Result:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.2 - f' n.1 n.2‖ < q
z : 𝕜
⊢ ‖z • g' n.2 - z • f' n.1 n.2‖ ≤ q * ‖z‖

Proof state:
case intro.intro
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_3
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst✝¹ : IsRCLikeNormedField 𝕜
inst✝ : l.NeBot
hf' : ∀ ε > 0, ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun n => f n y) l (𝓝 (g y))
F' : ι → 𝕜 → 𝕜 →L[𝕜] G := fun n z => ContinuousLinearMap.smulRight 1 (f' n z)
G' : 𝕜 → 𝕜 →L[𝕜] G := fun z => ContinuousLinearMap.smulRight 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (ContinuousLinearMap.smulRight 1 (f' n.1 n.2)) n.2
ε : ℝ
hε : ε > 0
q : ℝ
hq : 0 < q
hq' : q < ε
n : ι × 𝕜
hn : ‖g' n.2 - f' n.1 n.2‖ < q
z : 𝕜
⊢ ‖g' n.2 - f' n.1 n.2‖ * ‖z‖ ≤ q * ‖z‖

Tactic:
gcongr

Result:
no goals