awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
fun :
  UniformCauchySeqOnFilter.{u_5, u_7, u_1} (β := G)
    (fun (n : ι) (y : E) ↦ HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (f n y - f n x)) l (𝓝 x)
⊢ TendstoUniformlyOnFilter.{u_5, u_7, u_1} (β := G)
    (fun (n : ι) (y : E) ↦ HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (f n y - f n x))
    (fun (y : E) ↦ HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (g y - g x)) l (𝓝 x)

Tactic:
refine
    UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto ?_
      ((hfg.and (eventually_const.mpr hfg.self_of_nhds)).mono fun y hy =>
        (hy.1.sub hy.2).const_smul _)

Premises used: Iff.mpr, Filter.Eventually.self_of_nhds, Filter.Eventually.and, UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto, Filter.Eventually.mono, Filter.Tendsto.const_smul, And.right, And.left, Filter.eventually_const, Filter.Tendsto.sub
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
rw :
  TendstoUniformlyOnFilter.{u_5, u_7, u_1} (β := G)
    (fun (n : ι × ι) (z : E) ↦
      -HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖z - x‖ : 𝕜)⁻¹ (f n.1 z - f n.1 x) +
        HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖z - x‖ : 𝕜)⁻¹ (f n.2 z - f n.2 x))
    0 (l ×ˢ l) (𝓝 x)
⊢ UniformCauchySeqOnFilter.{u_5, u_7, u_1} (β := G)
    (fun (n : ι) (y : E) ↦ HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (f n y - f n x)) l (𝓝 x)

Tactic:
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero]

Premises used: SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
rw :
  ∀ ε > 0,
    ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2)
          (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.1 n.2 - f n.1.1 x) +
            HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.2 n.2 - f n.1.2 x)) <
        ε
⊢ TendstoUniformlyOnFilter.{u_5, u_7, u_1} (β := G)
    (fun (n : ι × ι) (z : E) ↦
      -HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖z - x‖ : 𝕜)⁻¹ (f n.1 z - f n.1 x) +
        HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖z - x‖ : 𝕜)⁻¹ (f n.2 z - f n.2 x))
    0 (l ×ˢ l) (𝓝 x)

Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff]

Premises used: Metric.tendstoUniformlyOnFilter_iff
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniformCauchySeqOnFilter f' l (𝓝 x)

Tactic:
have hfg' := hf'.uniformCauchySeqOnFilter
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : UniformCauchySeqOnFilter f' l (𝓝 x)
⊢ TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)

Tactic:
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hfg'

Premises used: SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
⊢ ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε

Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff] at hfg'

Premises used: Metric.tendstoUniformlyOnFilter_iff
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
obtain :
  ∀ (q : ℚ) (hqpos : 0 < q) (hqε : (↑q : ℝ) < ε),
    ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2)
          (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.1 n.2 - f n.1.1 x) +
            HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.2 n.2 - f n.1.2 x)) <
        ε
⊢ ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    dist (0 n.2)
        (-HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.1 n.2 - f n.1.1 x) +
          HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖n.2 - x‖ : 𝕜)⁻¹ (f n.1.2 n.2 - f n.1.2 x)) <
      ε

Tactic:
obtain ⟨q, hqpos, hqε⟩ := exists_pos_rat_lt hε

Premises used: exists_pos_rat_lt
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : (↑q : ℝ) < ε
⊢ GT.gt (α := ℝ) (↑q : ℝ) 0

Tactic:
simp [hqpos]
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : (↑q : ℝ) < ε
⊢ ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < (↑q : ℝ)

Tactic:
specialize hfg' (q : ℝ) (by simp [hqpos])

Premises used: Rat.cast
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : (↑q : ℝ) < ε
hfg' : ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < (↑q : ℝ)
⊢ ∀ᶠ (x : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧
      HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2

Tactic:
have := (tendsto_swap4_prod.eventually (hf.prod_mk hf)).diag_of_prod_right
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : (↑q : ℝ) < ε
hfg' : ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < (↑q : ℝ)
this :
  ∀ᶠ (x : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧
      HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2
a : ι × ι → Prop
b : ∀ᶠ (x : ι × ι) in l ×ˢ l, a x
c : E → Prop
d : ∀ᶠ (y : E) in 𝓝 x, c y
r : ℝ
hr : 0 < r
hr' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x r → c x_1
n : ι × ι
hn : a n
y : E
hy : (fun (e : E) ↦ Metric.ball x r e) y
hyz' : ¬x = y
hyz : 0 < ‖y - x‖
e :
  ∀ {x : ι × ι},
    a x →
      ∀ {y : E},
        c y →
          ‖f' x.1 y - f' x.2 y‖ < (↑q : ℝ) ∧
            HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f x.1) (f' x.1 y) y ∧
              HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f x.2) (f' x.2 y) y
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ ≤ (↑q : ℝ) * ‖y - x‖

Tactic:
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
      (fun y hy => ((e hn (hr' hy)).2.1.sub (e hn (hr' hy)).2.2).hasFDerivWithinAt)
      (fun y hy => (e hn (hr' hy)).1.le) (convex_ball x r) (Metric.mem_ball_self hr) hy

Premises used: HasFDerivAt.sub, HasFDerivAt.hasFDerivWithinAt, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, Metric.mem_ball_self, LT.lt.le, convex_ball, And.right, And.left
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
q : ℚ
hqpos : 0 < q
hqε : (↑q : ℝ) < ε
hfg' : ∀ᶠ (n : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < (↑q : ℝ)
this :
  ∀ᶠ (x : Prod.{u_1, u_5} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2 ∧
      HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜)
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1)
        (f' (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
          (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2)
        (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2
a : ι × ι → Prop
b : ∀ᶠ (x : ι × ι) in l ×ˢ l, a x
c : E → Prop
d : ∀ᶠ (y : E) in 𝓝 x, c y
r : ℝ
hr : 0 < r
hr' : ∀ ⦃x_1 : E⦄, x_1 ∈ Metric.ball x r → c x_1
n : ι × ι
hn : a n
y : E
hy : (fun (e : E) ↦ Metric.ball x r e) y
hyz' : ¬x = y
hyz : 0 < ‖y - x‖
e :
  ∀ {x : ι × ι},
    a x →
      ∀ {y : E},
        c y →
          ‖f' x.1 y - f' x.2 y‖ < (↑q : ℝ) ∧
            HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f x.1) (f' x.1 y) y ∧
              HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f x.2) (f' x.2 y) y
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ ≤ (↑q : ℝ) * ‖y - x‖

Tactic:
refine
    Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
      (fun y hy => ((e hn (hr' hy)).2.1.sub (e hn (hr' hy)).2.2).hasFDerivWithinAt)
      (fun y hy => (e hn (hr' hy)).1.le) (convex_ball x r) (Metric.mem_ball_self hr) hy

Premises used: HasFDerivAt.sub, HasFDerivAt.hasFDerivWithinAt, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le, Metric.mem_ball_self, LT.lt.le, convex_ball, And.right, And.left
-- 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
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 𝕜
rw :
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := G) (g x' - g x) ((g' x : (a : E) → G) (x' - x) : G)‖)
    (𝓝 x) (𝓝 0)
⊢ HasFDerivAt g (g' x) x

Tactic:
rw [hasFDerivAt_iff_tendsto]

Premises used: hasFDerivAt_iff_tendsto
-- 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
x : E
inst_6 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this :
  Tendsto (β := ℝ)
    (fun (y : ι × E) ↦ ‖y.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g y.2 - g x) ((g' x : (a : E) → G) (y.2 - x) : G)‖)
    (l.curry (𝓝 x)) (𝓝 0)
rw :
  ∀
    (this :
      ∀ ε > 0,
        ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
          dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε),
    ∀ ε > 0,
      ∀ᶠ (x_1 : E) in 𝓝 x,
        dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε
⊢ Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := G) (g x' - g x) ((g' x : (a : E) → G) (x' - x) : G)‖)
    (𝓝 x) (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds] at this ⊢

Premises used: Metric.tendsto_nhds
-- 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
x : E
inst_6 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this :
  ∀ ε > 0,
    ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
      dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε

Tactic:
specialize this ε hε
-- 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
x : E
inst_6 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
ε : ℝ
hε : ε > 0
this :
  ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist (‖x_1.2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1.2 - g x) ((g' x : (a : E) → G) (x_1.2 - x) : G)‖) 0 < ε
⊢ ∀ᶠ (x_1 : ι) in l,
    ∀ᶠ (y : E) in 𝓝 x,
      dist (‖(x_1, y).2 - x‖⁻¹ * ‖HSub.hSub (β := G) (g (x_1, y).2 - g x) ((g' x : (a : E) → G) ((x_1, y).2 - x) : G)‖)
          0 <
        ε

Tactic:
rw [eventually_curry_iff] at this

Premises used: Filter.eventually_curry_iff
-- 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
x : E
inst_6 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
ε : ℝ
hε : ε > 0
this :
  ∀ᶠ (x_1 : ι) in l,
    ∀ᶠ (y : E) in 𝓝 x, dist (‖y - x‖⁻¹ * ‖HSub.hSub (β := G) (g y - g x) ((g' x : (a : E) → G) (y - x) : G)‖) 0 < ε
⊢ ∀ (x_1 : E),
    dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε →
      dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε

Tactic:
simp only [imp_self, forall_const]

Premises used: imp_self, forall_const
-- 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
x : E
inst_6 : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
ε : ℝ
hε : ε > 0
this :
  ∀ᶠ (x_1 : ι) in l,
    ∀ᶠ (y : E) in 𝓝 x, dist (‖y - x‖⁻¹ * ‖HSub.hSub (β := G) (g y - g x) ((g' x : (a : E) → G) (y - x) : G)‖) 0 < ε
⊢ ∀ᶠ (x_1 : E) in 𝓝 x,
    dist (‖x_1 - x‖⁻¹ * ‖HSub.hSub (β := G) (g x_1 - g x) ((g' x : (a : E) → G) (x_1 - x) : G)‖) 0 < ε

Tactic:
exact (eventually_const.mp this).mono (by simp only [imp_self, forall_const])

Premises used: Filter.Eventually.mono, Filter.eventually_const, Iff.mp