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 : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
h1 : Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (β := E →L[𝕜] G) (fun (n : ι) ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
⊢ 0 < ‖n.2 - x‖
have rw : n.2 - x ≠ 0
Tactic: rw [norm_pos_iff]
-- 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)
h1 : Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (β := E →L[𝕜] G) (fun (n : ι) ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
⊢ ‖n.2 - x‖⁻¹ * norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤
    norm (E := E →L[𝕜] G) ((Prod.fst ∘ Prod.map (fun (n : ι) ↦ g' x - f' n x) id) n)
have hnx : 0 < ‖n.2 - x‖
Tactic: have hnx : 0 < ‖n.2 - x‖ := by
      rw [norm_pos_iff]; intro hx'; exact hx (eq_of_sub_eq_zero hx').symm
-- 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)
h1 : Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (β := E →L[𝕜] G) (fun (n : ι) ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
hnx : 0 < ‖n.2 - x‖
⊢ ‖n.2 - x‖⁻¹ * norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤
    norm (E := E →L[𝕜] G) ((Prod.fst ∘ Prod.map (fun (n : ι) ↦ g' x - f' n x) id) n)
have neg : norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤
  norm (E := E →L[𝕜] G) ((Prod.fst ∘ Prod.map (fun (n : ι) ↦ g' x - f' n x) id) n) * ‖n.2 - x‖
Tactic: rw [inv_mul_le_iff₀ hnx, mul_comm]
-- 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)
h1 : Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (β := E →L[𝕜] G) (fun (n : ι) ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
hnx : 0 < ‖n.2 - x‖
⊢ norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤
    norm (E := E →L[𝕜] G) ((Prod.fst ∘ Prod.map (fun (n : ι) ↦ g' x - f' n x) id) n) * ‖n.2 - x‖
have neg : norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤ ‖g' x - f' n.1 x‖ * ‖n.2 - x‖
Tactic: simp only [Function.comp_apply, Prod.map_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_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 :
  (fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
        (HSub.hSub (β := G) (g a.2 - g x) ((g' x : (a : E) → G) (a.2 - x) : G))) =
    (HAdd.hAdd (α := (a : ι × E) → G)
        (fun (a : ι × E) ↦
          HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹ (g a.2 - g x - (f a.1 a.2 - f a.1 x)))
        fun (a : ι × E) ↦
        HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (↑‖a.2 - x‖ : 𝕜)⁻¹
          (f a.1 a.2 - f a.1 x -
            HSub.hSub (α := G) (β := G) ((f' a.1 x : (a : E) → G) a.2 : G) ((f' a.1 x : (a : E) → G) x : G))) +
      fun (a : ι × E) ↦
      HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (β := G) (↑‖a.2 - x‖ : 𝕜)⁻¹ ((f' a.1 x - g' x : (a : E) → G) (a.2 - x) : G)
this : 𝓝 0 = 𝓝 (HAdd.hAdd (α := G) 0 0 + 0)
h1 : Tendsto (β := E →L[𝕜] G) (fun (n : ι × E) ↦ g' n.2 - f' n.1 n.2) (l ×ˢ 𝓝 x) (𝓝 0)
h2 : Tendsto (β := E →L[𝕜] G) (fun (n : ι) ↦ g' x - f' n x) l (𝓝 0)
n : ι × E
hx : ¬x = n.2
hnx : 0 < ‖n.2 - x‖
⊢ norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤ ‖g' x - f' n.1 x‖ * ‖n.2 - x‖
have neg : norm.{u_4} (E := G) ((f' n.1 x - g' x : (a : E) → G) (n.2 - x) : G) ≤ ‖f' n.1 x - g' x‖ * ‖n.2 - x‖
Tactic: rw [norm_sub_rev]
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasFDerivAt g (g' x) x
have h1 : s ∈ 𝓝 x
Tactic: have h1 : s ∈ 𝓝 x := hs.mem_nhds hx
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
⊢ HasFDerivAt g (g' x) x
have h3 : SProd.sprod (α := Set ι) Set.univ s ∈ l ×ˢ 𝓝 x
Tactic: have h3 : Set.univ ×ˢ s ∈ l ×ˢ 𝓝 x := by simp only [h1, prod_mem_prod_iff, univ_mem, and_self_iff]
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
h3 : SProd.sprod (α := Set ι) Set.univ s ∈ l ×ˢ 𝓝 x
⊢ HasFDerivAt g (g' x) x
have h4 : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
Tactic: have h4 : ∀ᶠ n : ι × E in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2 :=
    eventually_of_mem h3 fun ⟨n, z⟩ ⟨_, hz⟩ => hf n z hz
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ (n : ι), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
h3 : SProd.sprod (α := Set ι) Set.univ s ∈ l ×ˢ 𝓝 x
h4 : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
⊢ HasFDerivAt g (g' x) x
have refine : TendstoUniformlyOnFilter f' g' l (𝓝 x)
Tactic: refine hasFDerivAt_of_tendstoUniformlyOnFilter ?_ h4 (eventually_of_mem h1 hfg)
-- 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
g' : E → E →L[𝕜] G
x : E
inst_6 : l.NeBot
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasFDerivAt g (g' x) x
have refine : ∀ (n : ι) (z : E) (hz : z ∈ s), HasFDerivAt.{u_3, u_2, u_4} (𝕜 := 𝕜) (f n) ((fderiv 𝕜 ∘ f) n z) z
Tactic: refine hasFDerivAt_of_tendstoLocallyUniformlyOn hs hf' (fun n z hz => ?_) hfg hx
-- 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
inst_6 : l.NeBot
hf' : TendstoUniformly f' g' l
hf : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x
hfg : ∀ (x : E), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : E
⊢ HasFDerivAt g (g' x) x
have hf₁ : ∀ (n : ι) (x : E), Membership.mem (γ := Set E) Set.univ x → HasFDerivAt (f n) (f' n x) x
Tactic: have hf : ∀ n : ι, ∀ x : E, x ∈ Set.univ → HasFDerivAt (f n) (f' n x) x := by simp [hf]
-- 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
inst_6 : l.NeBot
hf' : TendstoUniformly f' g' l
hf_1 : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x
hfg : ∀ (x : E), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : E
hf : ∀ (n : ι) (x : E), Membership.mem (γ := Set E) Set.univ x → HasFDerivAt (f n) (f' n x) x
⊢ HasFDerivAt g (g' x) x
have hfg₁ : ∀ (x : E), Membership.mem (γ := Set E) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
Tactic: have hfg : ∀ x : E, x ∈ Set.univ → Tendsto (fun n => f n x) l (𝓝 (g x)) := by simp [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
inst_6 : l.NeBot
hf' : TendstoUniformly f' g' l
hf_1 : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x
hfg_1 : ∀ (x : E), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : E
hf : ∀ (n : ι) (x : E), Membership.mem (γ := Set E) Set.univ x → HasFDerivAt (f n) (f' n x) x
hfg : ∀ (x : E), Membership.mem (γ := Set E) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
⊢ HasFDerivAt g (g' x) x
have hf'₁ : TendstoUniformlyOn f' g' l Set.univ
Tactic: have hf' : TendstoUniformlyOn f' g' l Set.univ := by rwa [tendstoUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_3} (α := G) (map (fun (n : ι) ↦ f n x) l)
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
have hf₁ : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (𝕜 := 𝕜) (f n.1) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n.1 n.2)) n.2
Tactic: simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_3} (α := G) (map (fun (n : ι) ↦ f n x) l)
⊢ UniformCauchySeqOn f l (Metric.ball x r)
have hf₁ : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (𝕜 := 𝕜) (f n) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n y)) y
Tactic: simp_rw [hasDerivAt_iff_hasFDerivAt] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f f' : ι → 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hfg : Cauchy.{u_3} (α := G) (map (fun (n : ι) ↦ f n x) l)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (𝕜 := 𝕜) (f n) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n y)) y
⊢ UniformCauchySeqOn f l (Metric.ball x r)
have hf'₁ : UniformCauchySeqOn (β := 𝕜 →L[𝕜] G) (fun (n : ι) (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z)) l
  (Metric.ball x r)
Tactic: have hf' :
    UniformCauchySeqOn (fun n => fun z => (1 : 𝕜 →L[𝕜] 𝕜).smulRight (f' n z)) l
      (Metric.ball x r) :=
    (ContinuousLinearMap.smulRightL 𝕜 𝕜 G 1).uniformContinuous.comp_uniformCauchySeqOn hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
F' : (n : ι) → (z : 𝕜) → 𝕜 →L[𝕜] G := fun (n : ι) (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z)
G' : (z : 𝕜) → 𝕜 →L[𝕜] G := fun (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (g' z)
⊢ HasDerivAt g (g' x) x
have hf₁ : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (𝕜 := 𝕜) (f n.1) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n.1 n.2)) n.2
Tactic: simp_rw [hasDerivAt_iff_hasFDerivAt] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hfg : ∀ᶠ (y : 𝕜) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
F' : (n : ι) → (z : 𝕜) → 𝕜 →L[𝕜] G := fun (n : ι) (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z)
G' : (z : 𝕜) → 𝕜 →L[𝕜] G := fun (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (g' z)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (𝕜 := 𝕜) (f n.1) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n.1 n.2)) n.2
⊢ HasFDerivAt (𝕜 := 𝕜) g (ContinuousLinearMap.toSpanSingleton 𝕜 (g' x)) x
have hf'₁ : TendstoUniformlyOnFilter F' G' l (𝓝 x)
Tactic: have hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x) :=
    (ContinuousLinearMap.smulRightL 𝕜 𝕜 G 1).uniformContinuous.comp_tendstoUniformlyOnFilter hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasDerivAt g (g' x) x
have h1 : s ∈ 𝓝 x
Tactic: have h1 : s ∈ 𝓝 x := hs.mem_nhds hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
⊢ HasDerivAt g (g' x) x
have h2 : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
Tactic: have h2 : ∀ᶠ n : ι × 𝕜 in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2 :=
    eventually_prod_iff.2 ⟨_, hf, fun x => x ∈ s, h1, fun {n} => id⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g : 𝕜 → G
f' : ι → 𝕜 → G
g' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn f' g' l s
hf : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
h1 : s ∈ 𝓝 x
h2 : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasDerivAt (f n.1) (f' n.1 n.2) n.2
⊢ HasDerivAt g (g' x) x
have refine : TendstoUniformlyOnFilter f' g' l (𝓝 x)
Tactic: refine hasDerivAt_of_tendstoUniformlyOnFilter ?_ h2 (eventually_of_mem h1 hfg)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
G : Type u_3
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
f : ι → 𝕜 → G
g g' : 𝕜 → G
x : 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
s : Set 𝕜
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf' : TendstoLocallyUniformlyOn (deriv ∘ f) g' l s
hf : ∀ᶠ (n : ι) in l, DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasDerivAt g (g' x) x
have refine : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x
Tactic: refine hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' ?_ hfg hx