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_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
⊢ 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 refine_1 : ∀ ε > 0,
  ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε
Tactic: rw [Metric.tendsto_nhds]
-- 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_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε
have refine_1 : ∀ (x_1 : ι × E),
  dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x))
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (f x_1.1 x_1.2 - f x_1.1 x)) <
      ε →
    dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖x_1.2 - x‖ : 𝕜)⁻¹ (g x_1.2 - g x - (f x_1.1 x_1.2 - f x_1.1 x))) 0 < ε
Tactic: apply ((this ε hε).filter_mono curry_le_prod).mono
-- 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_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
n : ι × E
hn :
  dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
      (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
    ε
⊢ dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x))) 0 < ε
have refine_1 : ∀
  (hn :
    ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)‖ <
      ε),
  ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x)) - 0‖ < ε
Tactic: rw [dist_eq_norm] at hn ⊢
Cleared hypotheses: hn
-- 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_3 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
this :
  ∀ ε > 0,
    ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x,
      dist (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x))
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)) <
        ε
ε : ℝ
hε : ε > 0
n : ι × E
hn :
  ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)‖ <
    ε
⊢ ‖HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x)) - 0‖ < ε
have h : HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x - (f n.1 n.2 - f n.1 x)) - 0 =
  HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (g n.2 - g x) -
    HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1 n.2 - f n.1 x)
Tactic: convert! hn using 2
-- 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 (β := 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)
have refine_2 : ∀ ε > 0,
  ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist
        (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)))
        0 <
      ε
Tactic: rw [Metric.tendsto_nhds]
-- 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)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist
        (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)))
        0 <
      ε
have refine_2 : ∀ᶠ (x_1 : ι) in l,
  ∀ᶠ (y : E) in 𝓝 x,
    dist
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(x_1, y).2 - x‖ : 𝕜)⁻¹
          (f (x_1, y).1 (x_1, y).2 - f (x_1, y).1 x -
            HSub.hSub (α := G) (β := G) ((f' (x_1, y).1 x : (a : E) → G) (x_1, y).2 : G)
              ((f' (x_1, y).1 x : (a : E) → G) x : G)))
        0 <
      ε
Tactic: rw [eventually_curry_iff]
-- 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)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x_1 : ι) in l,
    ∀ᶠ (y : E) in 𝓝 x,
      dist
          (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(x_1, y).2 - x‖ : 𝕜)⁻¹
            (f (x_1, y).1 (x_1, y).2 - f (x_1, y).1 x -
              HSub.hSub (α := G) (β := G) ((f' (x_1, y).1 x : (a : E) → G) (x_1, y).2 : G)
                ((f' (x_1, y).1 x : (a : E) → G) x : G)))
          0 <
        ε
have refine_2 : ∀ (n : ι) (hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2),
  ∀ᶠ (y : E) in 𝓝 x,
    dist
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(n, y).2 - x‖ : 𝕜)⁻¹
          (f (n, y).1 (n, y).2 - f (n, y).1 x -
            HSub.hSub (α := G) (β := G) ((f' (n, y).1 x : (a : E) → G) (n, y).2 : G)
              ((f' (n, y).1 x : (a : E) → G) x : G)))
        0 <
      ε
Tactic: refine hf.curry.mono fun n hn => ?_
-- 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)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
⊢ ∀ᶠ (y : E) in 𝓝 x,
    dist
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(n, y).2 - x‖ : 𝕜)⁻¹
          (f (n, y).1 (n, y).2 - f (n, y).1 x -
            HSub.hSub (α := G) (β := G) ((f' (n, y).1 x : (a : E) → G) (n, y).2 : G)
              ((f' (n, y).1 x : (a : E) → G) x : G)))
        0 <
      ε
have this₁ : HasFDerivAt (f (n, x).1) (f' (n, x).1 (n, x).2) (n, x).2
Tactic: have := hn.self_of_nhds
-- 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)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this : HasFDerivAt (f (n, x).1) (f' (n, x).1 (n, x).2) (n, x).2
⊢ ∀ᶠ (y : E) in 𝓝 x,
    dist
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(n, y).2 - x‖ : 𝕜)⁻¹
          (f (n, y).1 (n, y).2 - f (n, y).1 x -
            HSub.hSub (α := G) (β := G) ((f' (n, y).1 x : (a : E) → G) (n, y).2 : G)
              ((f' (n, y).1 x : (a : E) → G) x : G)))
        0 <
      ε
have 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 <
      ε
Tactic: rw [hasFDerivAt_iff_tendsto, Metric.tendsto_nhds] 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_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) in 𝓝 x,
    dist
        (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(n, y).2 - x‖ : 𝕜)⁻¹
          (f (n, y).1 (n, y).2 - f (n, y).1 x -
            HSub.hSub (α := G) (β := G) ((f' (n, y).1 x : (a : E) → G) (n, y).2 : G)
              ((f' (n, y).1 x : (a : E) → G) x : G)))
        0 <
      ε
have refine_2 : ∀ (y : E)
  (hy :
    dist
        (‖y - (n, x).2‖⁻¹ *
          ‖HSub.hSub (β := G) (f (n, x).1 y - f (n, x).1 (n, x).2)
              ((f' (n, x).1 (n, x).2 : (a : E) → G) (y - (n, x).2) : G)‖)
        0 <
      ε),
  dist
      (HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖(n, y).2 - x‖ : 𝕜)⁻¹
        (f (n, y).1 (n, y).2 - f (n, y).1 x -
          HSub.hSub (α := G) (β := G) ((f' (n, y).1 x : (a : E) → G) (n, y).2 : G)
            ((f' (n, y).1 x : (a : E) → G) x : G)))
      0 <
    ε
Tactic: refine (this ε hε).mono fun y hy => ?_