awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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‖ : 𝕜)⁻¹
      (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))
have 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)
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 𝕜
x_1 : ι × E
⊢ 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)
have 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))
Tactic: simp only [map_sub, sub_add_sub_cancel, ContinuousLinearMap.coe_sub', Pi.sub_apply]
-- 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 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ 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)
have 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)
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
-- 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 :
  (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)
⊢ 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)
have 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)
Tactic: simp_rw [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 :
  (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)
⊢ 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)
have this₁ : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
Tactic: have : 𝓝 (0 : G) = 𝓝 (0 + 0 + 0) := by simp only [add_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_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)) (𝓝 0)
have 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))
Tactic: rw [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_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))
have 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)
Tactic: refine Tendsto.add (Tendsto.add ?_ ?_) ?_
-- 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_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)
⊢ 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))
have 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)
Tactic: refine Tendsto.add (Tendsto.add ?_ ?_) ?_
-- 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_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)
⊢ 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))
have 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)
Tactic: refine Tendsto.add (Tendsto.add ?_ ?_) ?_
-- 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_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} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
    (l.curry (𝓝 x)) (𝓝 0)
have 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)
Tactic: have := difference_quotients_converge_uniformly hf' hf hfg
-- 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_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)
⊢ 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)
have 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)) <
      ε
Tactic: rw [Metric.tendstoUniformlyOnFilter_iff] at this
Cleared hypotheses: this