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
f' : ι → E → E →L[𝕜] G
x : E
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
t : Set G
ht : Membership.mem (γ := Filter G) (map (fun (n : ι) ↦ f n x) l) t
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
⊢ ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f n.1.1 x - f n.1.2 x) < ε

Tactic:
exact
      eventually_prod_iff.mpr
        ⟨fun n : ι × ι => f n.1 x ∈ t ∧ f n.2 x ∈ t,
          eventually_prod_iff.mpr ⟨_, ht, _, ht, fun {n} hn {n'} hn' => ⟨hn, hn'⟩⟩,
          fun _ => True,
          by simp,
          fun {n} hn {y} _ => by simpa [norm_sub_rev, dist_eq_norm] using ht' _ hn.1 _ hn.2⟩

Premises used: Iff.mpr, Membership.mem, Prod.fst, Filter.eventually_prod_iff, And, And.intro, True, Exists.intro, Prod.snd
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ l.NeBot

Tactic:
have : NeBot l := (cauchy_map_iff.1 hfg).1
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
inl : ∀ (hr : r ≤ 0), UniformCauchySeqOn f l (Metric.ball x r)
inr : ∀ (hr : 0 < r), UniformCauchySeqOn f l (Metric.ball x r)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
rcases le_or_gt r 0 with (hr | hr)

Premises used: le_or_gt, OfNat.ofNat
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : r ≤ 0
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
simp only [Metric.ball_eq_empty.2 hr, UniformCauchySeqOn, Set.mem_empty_iff_false,
      IsEmpty.forall_iff, eventually_const, imp_true_iff]

Premises used: Iff.mpr, imp_true_iff, Filter.eventually_const, UniformCauchySeqOn, Metric.ball_eq_empty, Set.mem_empty_iff_false, IsEmpty.forall_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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf' : UniformCauchySeqOn f' l (Metric.ball x r)
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
inr :
  ∀
    (hf' :
      TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r))
    (this : l.NeBot) (hr : 0 < r),
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l)
      (Metric.ball x r)
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
rw [SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero] at hf' ⊢

Premises used: SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
⊢ TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    (HAdd.hAdd (α := E → G) (-0) (-0)) (l ×ˢ l) (Metric.ball x r)

Tactic:
have := this.1.neg.add this.2.neg
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    (HAdd.hAdd (α := E → G) (-0) (-0)) (l ×ˢ l) (Metric.ball x r)
⊢ TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)

Tactic:
rw [neg_zero, add_zero] at this

Premises used: add_zero, neg_zero
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)
⊢ TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l)
    (Metric.ball x r)

Tactic:
this.congr ?_

Premises used: TendstoUniformlyOn.congr
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)
refine :
  ∀ᶠ (n : ι × ι) in l ×ˢ l,
    Set.EqOn
      (HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
        (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
        (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) n)
      (fun (z : E) ↦ -f n.1 z + f n.2 z) (Metric.ball x r)
⊢ TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l)
    (Metric.ball x r)

Tactic:
refine this.congr ?_

Premises used: TendstoUniformlyOn.congr
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)
n : ι × ι
z : E
h :
  z ∈ Metric.ball x r →
    HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
        (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
        (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) n z =
      (fun (z : E) ↦ -f n.1 z + f n.2 z) z
⊢ z ∈ Metric.ball x r →
    HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
        (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
        (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) n z =
      (fun (z : E) ↦ -f n.1 z + f n.2 z) z

Tactic:
_
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)
n : ι × ι
z : E
h : z ∈ Metric.ball x r
simp : f n.1 x - f n.2 x - (f n.1 z - f n.2 z) + (f n.2 x - f n.1 x) = -f n.1 z + f n.2 z
⊢ HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
      (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) n z =
    (fun (z : E) ↦ -f n.1 z + f n.2 z) z

Tactic:
simp
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)
n : ι × ι
z : E
h : z ∈ Metric.ball x r
⊢ f n.1 x - f n.2 x - (f n.1 z - f n.2 z) + (f n.2 x - f n.1 x) = -f n.1 z + f n.2 z

Tactic:
abel
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this_3 : l.NeBot
hr : 0 < r
this_4 :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
this :
  TendstoUniformlyOn
    (HAdd.hAdd (α := ι × ι → E → G) (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
      (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x))
    0 (l ×ˢ l) (Metric.ball x r)
h :
  ∀ (a : ι × ι),
    Membership.mem (γ := Set (ι × ι))
      {x_1 : ι × ι |
        (fun (n : ι × ι) ↦
            Set.EqOn
              (HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
                (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
                (-fun (n : ι × ι) (x_2 : E) ↦ f n.1 x - f n.2 x) n)
              (fun (z : E) ↦ -f n.1 z + f n.2 z) (Metric.ball x r))
          x_1}
      a
h₁ :
  ∀ (a : ι × ι),
    Set.EqOn
      (HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
        (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
        (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) a)
      (fun (z : E) ↦ -f a.1 z + f a.2 z) (Metric.ball x r)
h₂ :
  ∀ (n : ι × ι) ⦃z : E⦄,
    z ∈ Metric.ball x r →
      HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
          (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
          (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) n z =
        (fun (z : E) ↦ -f n.1 z + f n.2 z) z
⊢ ∀ᶠ (n : ι × ι) in l ×ˢ l,
    Set.EqOn
      (HAdd.hAdd (α := ι × ι → E → G) (β := ι × ι → E → G)
        (-fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x))
        (-fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) n)
      (fun (z : E) ↦ -f n.1 z + f n.2 z) (Metric.ball x r)

Tactic:
filter_upwards with n z _ using (by simp; abel)
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
inr :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)
⊢ TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l)
    (Metric.ball x r)

Tactic:
suffices
    TendstoUniformlyOn (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
        (l ×ˢ l) (Metric.ball x r) ∧
      TendstoUniformlyOn (fun (n : ι × ι) (_ : E) => f n.1 x - f n.2 x) 0
        (l ×ˢ l) (Metric.ball x r) by
    have := this.1.neg.add this.2.neg
    rw [neg_zero, add_zero] at this
    refine this.congr ?_
    filter_upwards with n z _ using (by simp; abel)
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
inr :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
    (l ×ˢ l) (Metric.ball x r)
inr₁ :
  TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
⊢ TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
      (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
      (Metric.ball x r)

Tactic:
constructor
-- 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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (β := E →L[𝕜] G) (fun (n : ι × ι) (z : E) ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
inr :
  ∀ (hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε)
    (this : l.NeBot) (hr : 0 < r),
    ∀ ε > 0,
      ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x_1 - f n.2 x_1 - (f n.1 x - f n.2 x)) < ε
⊢ TendstoUniformlyOn.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (z : E) ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
    (l ×ˢ l) (Metric.ball x r)

Tactic:
rw [Metric.tendstoUniformlyOn_iff] at hf' ⊢

Premises used: Metric.tendstoUniformlyOn_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
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
this_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
simp_rw : ∃ (q : ℝ), 0 < q ∧ r * q < ε
⊢ ∃ (q : ℝ), 0 < q ∧ q * r < ε

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm