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_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)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist
          (‖x_1 - (n, x).2‖⁻¹ *
            ‖HSub.hSub (β := G) (f (n, x).1 x_1 - f (n, x).1 (n, x).2)
                ((f' (n, x).1 (n, x).2 : (a : E) → G) (x_1 - (n, x).2) : G)‖)
          0 <
        ε
y : E
hy :
  ‖y - x‖⁻¹ *
      ‖f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G)‖ <
    ε
refine_2 :
  ‖y - x‖⁻¹ *
      ‖f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G)‖ <
    ε
⊢ ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹
        (f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G))‖ <
    ε

Tactic:
rw [norm_smul, norm_inv, RCLike.norm_coe_norm]

Premises used: norm_smul, norm_inv, RCLike.norm_coe_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)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist
          (‖x_1 - (n, x).2‖⁻¹ *
            ‖HSub.hSub (β := G) (f (n, x).1 x_1 - f (n, x).1 (n, x).2)
                ((f' (n, x).1 (n, x).2 : (a : E) → G) (x_1 - (n, x).2) : G)‖)
          0 <
        ε
y : E
hy :
  ‖y - x‖⁻¹ *
      ‖f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G)‖ <
    ε
⊢ ‖y - x‖⁻¹ *
      ‖f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G)‖ <
    ε

Tactic:
hy
-- 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)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 (n, x).2,
      dist
          (‖x_1 - (n, x).2‖⁻¹ *
            ‖HSub.hSub (β := G) (f (n, x).1 x_1 - f (n, x).1 (n, x).2)
                ((f' (n, x).1 (n, x).2 : (a : E) → G) (x_1 - (n, x).2) : G)‖)
          0 <
        ε
y : E
hy :
  ‖y - x‖⁻¹ *
      ‖f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G)‖ <
    ε
⊢ ‖y - x‖⁻¹ *
      ‖f n y - f n x - HSub.hSub (α := G) (β := G) ((f' n x : (a : E) → G) y : G) ((f' n x : (a : E) → G) x : G)‖ <
    ε

Tactic:
exact hy
-- 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 (β := 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:
Tendsto.mono_left ?_ curry_le_prod

Premises used: Filter.curry_le_prod, Filter.Tendsto.mono_left
-- 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_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 ×ˢ 𝓝 x) (𝓝 0)
⊢ 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)

Tactic:
refine Tendsto.mono_left ?_ curry_le_prod

Premises used: Filter.curry_le_prod, Filter.Tendsto.mono_left
-- 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)
⊢ ∀ ε > 0, ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε

Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff] at hf'

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 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
hf'₁ : ∀ ε > 0, ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.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)

Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff] at hf'

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 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
hf'₁ : ∀ ε > 0, ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
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:
rw [Metric.tendstoUniformlyOnFilter_iff] at hf'

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 : ∀ᶠ (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 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
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)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x : ι × E) in l ×ˢ 𝓝 x, dist (g' x.2 - f' x.1 x.2) 0 < ε

Tactic:
simpa [dist_eq_norm] using hf' ε hε

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 : ∀ᶠ (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 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, dist (g' n.2) (f' n.1 n.2) < ε
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 (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)

Tactic:
exact Metric.tendsto_nhds.mpr fun ε hε => by simpa [dist_eq_norm] using hf' ε hε

Premises used: Iff.mpr, 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 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
⊢ Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)

Tactic:
have h1 : Tendsto (fun n : ι × E => g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0) := by
      rw [Metric.tendstoUniformlyOnFilter_iff] at hf'
      exact Metric.tendsto_nhds.mpr fun ε hε => by simpa [dist_eq_norm] using hf' ε hε
-- 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)
h1 : Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
rw :
  ∀ (h1 : ∀ ε > 0, ∀ᶠ (x : ι × E) in l ×ˢ 𝓝 x, dist (g' x.2 - f' x.1 x.2) 0 < ε),
    ∀ ε > 0, ∀ᶠ (x_1 : ι) in l, dist (g' x - f' x_1 x) 0 < ε
⊢ Tendsto (β := E →L[𝕜] G) (fun (n : ι) ↦ g' x - f' n x) l (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds] at h1 ⊢

Premises used: Metric.tendsto_nhds