awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
⊢ 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)

Tactic:
have : 𝓝 (0 : G) = 𝓝 (0 + 0 + 0) := by simp only [add_zero]
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
rw :
  Tendsto
    ((HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G))
    (l.curry (𝓝 x)) (𝓝 (HAdd.hAdd (α := G) 0 0 + 0))
⊢ Tendsto
    ((HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G))
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
rw [this]
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
⊢ Tendsto
    ((HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G))
    (l.curry (𝓝 x)) (𝓝 (HAdd.hAdd (α := G) 0 0 + 0))

Tactic:
Tendsto.add (Tendsto.add ?_ ?_) ?_

Premises used: Filter.Tendsto.add
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
refine_1 :
  Tendsto (β := G)
    (fun (a : ι × E) ↦ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
    (l.curry (𝓝 x)) (𝓝 0)
refine_2 :
  Tendsto (β := G)
    (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (f a.1 a.2 - f a.1 x -
          HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G)))
    (l.curry (𝓝 x)) (𝓝 0)
refine_3 :
  Tendsto (β := G)
    (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G))
    (l.curry (𝓝 x)) (𝓝 0)
⊢ Tendsto
    ((HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G))
    (l.curry (𝓝 x)) (𝓝 (HAdd.hAdd (α := G) 0 0 + 0))

Tactic:
refine Tendsto.add (Tendsto.add ?_ ?_) ?_

Premises used: Filter.Tendsto.add
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G)
    (fun (n : ι) (y : E) ↦ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (f n y - f n x))
    (fun (y : E) ↦ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (g y - g x)) l (𝓝 x)

Tactic:
have := difference_quotients_converge_uniformly hf' hf hfg
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G)
    (fun (n : ι) (y : E) ↦ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (f n y - f n x))
    (fun (y : E) ↦ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (g y - g x)) l (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε

Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff] at this

Premises used: Metric.tendstoUniformlyOnFilter_iff
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
refine_1 :
  ∀ ε > 0,
    ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 <
        ε
⊢ Tendsto (β := G)
    (fun (a : ι × E) ↦ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds]

Premises used: Metric.tendsto_nhds
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
refine_1 :
  ∀ (x_1 : ι × E),
    dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (f x_1.1 x_1.2 - f x_1.1 x)) <
        ε →
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 <
        ε
⊢ ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε

Tactic:
apply ((this ε hε).filter_mono curry_le_prod).mono

Premises used: Filter.Eventually.filter_mono, Filter.curry_le_prod, Filter.Eventually.mono
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
n : ι × E
hn :
  dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
      (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
    ε
refine_1 :
  ∀
    (hn :
      ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
            HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)‖ <
        ε),
    ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x)) - 0‖ < ε
⊢ dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x))) 0 < ε

Tactic:
rw [dist_eq_norm] at hn ⊢

Premises used: dist_eq_norm
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
n : ι × E
hn :
  ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)‖ <
    ε
⊢ ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)‖ <
    ε

Tactic:
hn
-- 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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
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))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
n : ι × E
hn :
  ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)‖ <
    ε
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x)) - 0 =
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)
⊢ ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x)) - 0‖ < ε

Tactic:
convert! hn using 2