awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : 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.{u_6, u_5, u_7} (𝕜 := 𝕜) (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 : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < (↑q : ℝ)
⊢ ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2)
        (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.1 n.2 - f n.1.1 x) +
          HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.2 n.2 - f n.1.2 x)) <
      ε
have this : ∀ᶠ (x : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
  HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
      (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.{u_6, u_5, u_7} (𝕜 := 𝕜)
      (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
Tactic: have := (tendsto_swap4_prod.eventually (hf.prod_mk hf)).diag_of_prod_right
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 𝕜
⊢ HasFDerivAt g (g' x) x
have rw : Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := G) (g x' - g x) ((g' x : (a : E) → G) (x' - x) : G)‖)
  (𝓝 x) (𝓝 0)
Tactic: rw [hasFDerivAt_iff_tendsto]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 :
  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)
⊢ Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := G) (g x' - g x) ((g' x : (a : E) → G) (x' - x) : G)‖)
    (𝓝 x) (𝓝 0)
have rw : ∀
  (this :
    ∀ ε > 0,
      ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
        dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε),
  ∀ ε > 0,
    ∀ᶠ (x_1 : E) in 𝓝 x,
      dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε
Tactic: rw [Metric.tendsto_nhds] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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 :
  ∀ ε > 0,
    ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
      dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝 x,
    dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε
have this₁ : ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
  dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε
Tactic: specialize this ε hε
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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 𝕜
ε : ℝ
hε : ε > 0
this :
  ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝 x,
    dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε
have this₁ : ∀ᶠ (x_1 : ι) in l,
  ∀ᶠ (y : E) in 𝓝 x,
    dist (‖(x_1, y).2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g (x_1, y).2 - g x) ((g' x : (a : E) → G) ((x_1, y).2 - x) : G)‖)
        0 <
      ε
Tactic: rw [eventually_curry_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 𝕜
⊢ Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := G) (g x' - g x) ((g' x : (a : E) → G) (x' - x) : G)‖)
    (𝓝 x) (𝓝 0)
have Tendsto : 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: 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])
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 𝕜
| 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)
have f₁ : fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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)‖
| 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)
have l₁ : l.curry (𝓝 x)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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)
| 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)
have l₂ : 𝓝 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖
have 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)‖
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
| ‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖
have 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))‖
Tactic: rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 𝕜
| 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)
have 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))‖
Tactic: congr
    ext
    rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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))‖
| 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)
have l₁ : l.curry (𝓝 x)
Tactic: congr
    ext
    rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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)
| 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)
have l₂ : 𝓝 0
Tactic: congr
    ext
    rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 𝕜
⊢ 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)
have 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)
Tactic: conv =>
    congr
    ext
    rw [← abs_norm, ← abs_inv, ← @RCLike.norm_ofReal 𝕜 _ _, RCLike.ofReal_inv, ← norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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 𝕜
⊢ 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)
have 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)
Tactic: rw [← tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
⊢ 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
have 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)
Tactic: simp only [Pi.add_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
⊢ 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)
have 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))
Tactic: rw [← smul_add, ← smul_add]