awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
inst_6 : l.NeBot
hf'_1 : 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))
hf' : TendstoUniformlyOn f' g' l Set.univ
⊢ HasFDerivAt g (g' x) x

Tactic:
exact hasFDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)

Premises used: isOpen_univ, Set.mem_univ, hasFDerivAt_of_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
l' : Filter 𝕜
hf' : UniformCauchySeqOnFilter f' l l'
u : Set ((𝕜 →L[𝕜] G) × (𝕜 →L[𝕜] G))
hu : Membership.mem (γ := Filter ((𝕜 →L[𝕜] G) × (𝕜 →L[𝕜] G))) (uniformity (𝕜 →L[𝕜] G)) u
⊢ ∀ᶠ (m : Prod.{u_1, u_2} (ι × ι) 𝕜) in (l ×ˢ l) ×ˢ l',
    ((fun (n : ι) (z : 𝕜) ↦ (ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z) : 𝕜 →L[𝕜] G)) m.1.1 m.2,
        (fun (n : ι) (z : 𝕜) ↦ (ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z) : 𝕜 →L[𝕜] G)) m.1.2 m.2) ∈
      u

Tactic:
simpa using hf' _ ((ContinuousLinearMap.smulRightL 𝕜 𝕜 G 1).uniformContinuous hu)

Premises used: ContinuousLinearMap.uniformContinuous, ContinuousLinearMap.smulRightL, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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)
⊢ ∀ᶠ (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

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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)
hfg : Cauchy.{u_3} (α := G) (map (fun (n : ι) ↦ f n x) l)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (𝕜 := 𝕜) (f n.1) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n.1 n.2)) n.2
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
uniformCauchySeqOnFilter_of_fderiv hf'.one_smulRight hf hfg

Premises used: uniformCauchySeqOnFilter_of_fderiv, UniformCauchySeqOnFilter.one_smulRight
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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)
hfg : Cauchy.{u_3} (α := G) (map (fun (n : ι) ↦ f n x) l)
hf : ∀ᶠ (n : ι × 𝕜) in l ×ˢ 𝓝 x, HasFDerivAt (𝕜 := 𝕜) (f n.1) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n.1 n.2)) n.2
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
exact uniformCauchySeqOnFilter_of_fderiv hf'.one_smulRight hf hfg

Premises used: uniformCauchySeqOnFilter_of_fderiv, UniformCauchySeqOnFilter.one_smulRight
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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)
⊢ ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (𝕜 := 𝕜) (f n) (ContinuousLinearMap.toSpanSingleton 𝕜 (f' n y)) y

Tactic:
simp_rw [hasDerivAt_iff_hasFDerivAt] at hf

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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 (β := 𝕜 →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'
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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'_1 : 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
hf' :
  UniformCauchySeqOn (β := 𝕜 →L[𝕜] G) (fun (n : ι) (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z)) l
    (Metric.ball x r)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
uniformCauchySeqOn_ball_of_fderiv hf' hf hfg

Premises used: uniformCauchySeqOn_ball_of_fderiv
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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'_1 : 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
hf' :
  UniformCauchySeqOn (β := 𝕜 →L[𝕜] G) (fun (n : ι) (z : 𝕜) ↦ ContinuousLinearMap.smulRight (S := 𝕜) 1 (f' n z)) l
    (Metric.ball x r)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
exact uniformCauchySeqOn_ball_of_fderiv hf' hf hfg

Premises used: uniformCauchySeqOn_ball_of_fderiv
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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)
⊢ ∀ᶠ (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 ⊢

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
⊢ TendstoUniformlyOnFilter F' G' l (𝓝 x)

Tactic:
have hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x) :=
    (ContinuousLinearMap.smulRightL 𝕜 𝕜 G 1).uniformContinuous.comp_tendstoUniformlyOnFilter hf'
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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'_1 : 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
hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x)
⊢ HasFDerivAt (𝕜 := 𝕜) g (ContinuousLinearMap.toSpanSingleton 𝕜 (g' x)) x

Tactic:
hasFDerivAt_of_tendstoUniformlyOnFilter hf' hf hfg

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.toSpanSingleton, hasFDerivAt_of_tendstoUniformlyOnFilter, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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'_1 : 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
hf' : TendstoUniformlyOnFilter F' G' l (𝓝 x)
⊢ HasFDerivAt (𝕜 := 𝕜) g (ContinuousLinearMap.toSpanSingleton 𝕜 (g' x)) x

Tactic:
exact hasFDerivAt_of_tendstoUniformlyOnFilter hf' hf hfg

Premises used: hasFDerivAt_of_tendstoUniformlyOnFilter
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
⊢ s ∈ 𝓝 x

Tactic:
have h1 : s ∈ 𝓝 x := hs.mem_nhds hx
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
⊢ ∀ᶠ (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⟩
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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

Tactic:
hasDerivAt_of_tendstoUniformlyOnFilter ?_ h2 (eventually_of_mem h1 hfg)

Premises used: Filter.eventually_of_mem, hasDerivAt_of_tendstoUniformlyOnFilter
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
refine : TendstoUniformlyOnFilter f' g' l (𝓝 x)
⊢ HasDerivAt g (g' x) x

Tactic:
refine hasDerivAt_of_tendstoUniformlyOnFilter ?_ h2 (eventually_of_mem h1 hfg)

Premises used: Filter.eventually_of_mem, hasDerivAt_of_tendstoUniformlyOnFilter
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
⊢ TendstoUniformlyOnFilter f' g' l (𝓝 x)

Tactic:
simpa [IsOpen.nhdsWithin_eq hs hx] using tendstoLocallyUniformlyOn_iff_filter.mp hf' x hx

Premises used: IsOpen.nhdsWithin_eq, Iff.mp, tendstoLocallyUniformlyOn_iff_filter
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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

Tactic:
hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' ?_ hfg hx

Premises used: hasDerivAt_of_tendstoLocallyUniformlyOn
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
refine : ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x
⊢ HasDerivAt g (g' x) x

Tactic:
refine hasDerivAt_of_tendstoLocallyUniformlyOn hs hf' ?_ hfg hx

Premises used: hasDerivAt_of_tendstoLocallyUniformlyOn
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
n : ι
h : DifferentiableOn 𝕜 (f n) s
z : 𝕜
hz : z ∈ s
⊢ HasDerivAt (f n) ((deriv ∘ f) n z) z

Tactic:
((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt

Premises used: DifferentiableAt.hasDerivAt, DifferentiableWithinAt.differentiableAt, deriv, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ DifferentiableOn 𝕜 (f n) s) x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x) x} x}
      a
h₁ h₂ : ∀ (n : ι) (h : DifferentiableOn 𝕜 (f n) s) (z : 𝕜) (hz : z ∈ s), HasDerivAt (f n) ((deriv ∘ f) n z) z
⊢ ∀ᶠ (n : ι) in l, ∀ x ∈ s, HasDerivAt (f n) ((deriv ∘ f) n x) x

Tactic:
filter_upwards [hf] with n h z hz using ((h z hz).differentiableAt (hs.mem_nhds hz)).hasDerivAt
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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' : TendstoUniformlyOn 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

Tactic:
hasDerivAt_of_tendstoLocallyUniformlyOn hs hf'.tendstoLocallyUniformlyOn hf hfg hx

Premises used: hasDerivAt_of_tendstoLocallyUniformlyOn, TendstoUniformlyOn.tendstoLocallyUniformlyOn
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x_1 : 𝕜
n : ι
h : ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
x : 𝕜
h₁ : Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
⊢ Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x

Tactic:
_
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x_1 : 𝕜
n : ι
h : ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
x : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) Set.univ x
⊢ HasDerivAt (f n) (f' n x) x

Tactic:
h x
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x) x} x →
          Membership.mem (γ := Set ι)
            {x : ι | (fun (n : ι) ↦ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x) x}
            x}
      a
h₁ h₂ :
  ∀ (n : ι) (h : ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x) (x : 𝕜),
    Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
⊢ ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x

Tactic:
filter_upwards [hf] with n h x _ using h x
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
⊢ ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x

Tactic:
have hf : ∀ᶠ n in l, ∀ x : 𝕜, x ∈ Set.univ → HasDerivAt (f n) (f' n x) x := by
    filter_upwards [hf] with n h x _ using h x
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf_1 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
⊢ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))

Tactic:
simp [hfg]
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf_1 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
⊢ ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))

Tactic:
have hfg : ∀ x : 𝕜, x ∈ Set.univ → Tendsto (fun n => f n x) l (𝓝 (g x)) := by simp [hfg]
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
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
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : l.NeBot
hf' : TendstoUniformly f' g' l
hf_1 : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), HasDerivAt (f n) (f' n x) x
hfg_1 : ∀ (x : 𝕜), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
x : 𝕜
hf : ∀ᶠ (n : ι) in l, ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → HasDerivAt (f n) (f' n x) x
hfg : ∀ (x : 𝕜), Membership.mem (γ := Set 𝕜) Set.univ x → Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))
rwa rwa₁ rwa₂ rwa₃ : TendstoUniformly f' g' l
⊢ TendstoUniformlyOn f' g' l Set.univ

Tactic:
rwa [tendstoUniformlyOn_univ]

Premises used: tendstoUniformlyOn_univ