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, Filter.Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
Tendsto :
  Filter.Tendsto (β := ℝ)
    (fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖)
    (l.curry (𝓝 x)) (𝓝 0)
⊢ Filter.Tendsto (β := ℝ)
    (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := G) (g x' - g x) ((g' x : (a : E) → G) (x' - x) : G)‖) (𝓝 x) (𝓝 0)

Tactic:
suffices
    Tendsto (fun y : ι × E => ‖y.2 - x‖⁻¹ * ‖g y.2 - g x - (g' x) (y.2 - x)‖)
      (l.curry (𝓝 x)) (𝓝 0) by
    rw [Metric.tendsto_nhds] at this ⊢
    intro ε hε
    specialize this ε hε
    rw [eventually_curry_iff] at this
    simp only at this
    exact (eventually_const.mp this).mono (by simp only [imp_self, forall_const])
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
f₁ : fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖
l₁ : l.curry (𝓝 x)
l₂ : 𝓝 0
| Tendsto (β := ℝ)
    (fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖)
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
congr
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
f₁ : ∀ (x_1 : ι × E), ‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖
| fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖

Tactic:
ext
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : ι × E
f₁ :
  ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G))‖
| ‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖

Tactic:
rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]

Premises used: norm_smul, RCLike.norm_ofReal, abs_inv, abs_norm, RCLike.ofReal_inv
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
f₁ :
  ∀ (x_1 : ι × E),
    ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G))‖
l₁ : l.curry (𝓝 x)
l₂ : 𝓝 0
| Tendsto (β := ℝ)
    (fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖)
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
congr
    ext
    rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]

Premises used: norm_smul, RCLike.norm_ofReal, abs_inv, abs_norm, RCLike.ofReal_inv
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
conv :
  Tendsto (β := ℝ)
    (fun (x_1 : ι × E) ↦
      ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
          (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G))‖)
    (l.curry (𝓝 x)) (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖)
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
conv =>
    congr
    ext
    rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]

Premises used: norm_smul, RCLike.norm_ofReal, abs_inv, abs_norm, RCLike.ofReal_inv
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
rw :
  Tendsto (β := G)
    (fun (x_1 : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)))
    (l.curry (𝓝 x)) (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (x_1 : ι × E) ↦
      ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
          (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G))‖)
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
rw [← tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
h :
  ∀ (x_1 : ι × E),
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)) =
      HAdd.hAdd (β := (a : ι × E) → 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))
        x_1
⊢ (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:
ext
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : ι × E
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)) =
    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)) +
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
          (f x_1.1 x_1.2 - f x_1.1 x -
            HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G)) +
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
        ((f' x_1.1 x - g' x : (a : E) → G) (x_1.2 - x) : G)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)) =
    HAdd.hAdd (β := (a : ι × E) → 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))
      x_1

Tactic:
simp only [Pi.add_apply]

Premises used: Pi.add_apply
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : ι × E
h :
  HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HAdd.hAdd (β := G)
        (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x) +
          (f x_1.1 x_1.2 - f x_1.1 x -
            HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G)))
        ((f' x_1.1 x - g' x : (a : E) → G) (x_1.2 - x) : G))
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)) =
    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)) +
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
          (f x_1.1 x_1.2 - f x_1.1 x -
            HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G)) +
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
        ((f' x_1.1 x - g' x : (a : E) → G) (x_1.2 - x) : G)

Tactic:
rw [← smul_add, ← smul_add]

Premises used: smul_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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : ι × E
h :
  HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G) =
    HAdd.hAdd (β := G)
      (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x) +
        (f x_1.1 x_1.2 - f x_1.1 x -
          HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G)))
      ((f' x_1.1 x - g' x : (a : E) → G) (x_1.2 - x) : G)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
      (HAdd.hAdd (β := G)
        (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x) +
          (f x_1.1 x_1.2 - f x_1.1 x -
            HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G)))
        ((f' x_1.1 x - g' x : (a : E) → G) (x_1.2 - x) : G))

Tactic:
congr
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : ι × E
h :
  g x_1.2 - g x - HSub.hSub (α := G) (β := G) ((g' x : (a : E) → G) x_1.2 : G) ((g' x : (a : E) → G) x : G) =
    g x_1.2 - g x -
        HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G) +
      (HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((g' x : (a : E) → G) x_1.2 : G) -
        HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x : G) ((g' x : (a : E) → G) x : G))
⊢ HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G) =
    HAdd.hAdd (β := G)
      (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x) +
        (f x_1.1 x_1.2 - f x_1.1 x -
          HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G)))
      ((f' x_1.1 x - g' x : (a : E) → G) (x_1.2 - x) : G)

Tactic:
simp only [map_sub, sub_add_sub_cancel, ContinuousLinearMap.coe_sub', Pi.sub_apply]

Premises used: sub_add_sub_cancel, map_sub, ContinuousLinearMap.coe_sub', Pi.sub_apply
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_1 : ι × E
⊢ g x_1.2 - g x - HSub.hSub (α := G) (β := G) ((g' x : (a : E) → G) x_1.2 : G) ((g' x : (a : E) → G) x : G) =
    g x_1.2 - g x -
        HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((f' x_1.1 x : (a : E) → G) x : G) +
      (HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x_1.2 : G) ((g' x : (a : E) → G) x_1.2 : G) -
        HSub.hSub (α := G) (β := G) ((f' x_1.1 x : (a : E) → G) x : G) ((g' x : (a : E) → G) x : G))

Tactic:
abel
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ (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:
have :
    (fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (g a.2 - g x - (g' x) (a.2 - x))) =
      ((fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) +
          fun a : ι × E =>
          (‖a.2 - x‖⁻¹ : 𝕜) • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
        fun a : ι × E => (‖a.2 - x‖⁻¹ : 𝕜) • (f' a.1 x - g' x) (a.2 - x) := by
    ext; simp only [Pi.add_apply]; rw [← smul_add, ← smul_add]; congr
    simp only [map_sub, sub_add_sub_cancel, ContinuousLinearMap.coe_sub', Pi.sub_apply]
    abel
-- 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)
simp_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)) (𝓝 0)
⊢ Tendsto (β := G)
    (fun (x_1 : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)))
    (l.curry (𝓝 x)) (𝓝 0)

Tactic:
simp_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 :
  (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:
simp only [add_zero]

Premises used: add_zero