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
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' : ∀ ε > 0, ∀ᶠ (n : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
this_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
this :
  ∀ᶠ (x : Prod.{u_1, u_2} (ι × ι) E) in (l ×ˢ l) ×ˢ 𝓝 x,
    HasFDerivAt (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 (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
r : ℝ := min 1 R
hr : 0 < r
hr' : ∀ ⦃y : E⦄, y ∈ Metric.ball x r → c y
hxy : ∀ y ∈ Metric.ball x r, ‖y - x‖ < 1
hxyε : ∀ y ∈ Metric.ball x r, ε * ‖y - x‖ < ε
n : ι × ι
hn : a n
y : E
hy : (fun (e : E) ↦ Metric.ball x r e) y
e :
  ∀ {x : ι × ι},
    a x →
      ∀ {y : E}, c y → ‖f' x.1 y - f' x.2 y‖ < ε ∧ HasFDerivAt (f x.1) (f' x.1 y) y ∧ HasFDerivAt (f x.2) (f' x.2 y) y
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε
have left : ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ ≤ ε * ‖y - x‖
Tactic: refine lt_of_le_of_lt ?_ (hxyε y hy)
-- 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
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
⊢ TendstoUniformlyOnFilter.{u_2, u_4, u_1} (β := G) (fun (n : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)
have right : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (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: refine Metric.tendstoUniformlyOnFilter_iff.mpr fun ε hε => ?_
-- 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
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
⊢ ∀ᶠ (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) < ε
have right : ∀ (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: obtain ⟨t, ht, ht'⟩ := (Metric.cauchy_iff.mp hfg).2 ε hε
-- 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
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
⊢ UniformCauchySeqOn f l (Metric.ball x r)
have this₁ : l.NeBot
Tactic: have : NeBot l := (cauchy_map_iff.1 hfg).1
-- 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
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
⊢ UniformCauchySeqOn f l (Metric.ball x r)
have inl : ∀ (hr : r ≤ 0), UniformCauchySeqOn f l (Metric.ball x r)
Tactic: rcases le_or_gt r 0 with (hr | hr)
-- 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
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)
⊢ UniformCauchySeqOn f l (Metric.ball x r)
have inr : ∀ (hr : 0 < r), UniformCauchySeqOn f l (Metric.ball x r)
Tactic: rcases le_or_gt r 0 with (hr | hr)
-- 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
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
⊢ UniformCauchySeqOn f l (Metric.ball x r)
have 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)
Tactic: rw [SeminormedAddGroup.uniformCauchySeqOn_iff_tendstoUniformlyOn_zero] at hf' ⊢
Cleared hypotheses: hf', this_2, this, hr
-- 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
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.{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)
have 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)
Tactic: have := this.1.neg.add this.2.neg
-- 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
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.{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)
have 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)
Tactic: rw [neg_zero, add_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
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)
have 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)
Tactic: refine this.congr ?_
-- 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
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
have 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
Tactic: simp
-- 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
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 : ι × ι) 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)
have 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
Tactic: filter_upwards with n z _ using (by simp; abel)
-- 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
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
⊢ ∀ᶠ (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)
have 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)
Tactic: filter_upwards with n z _ using (by simp; abel)
-- 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
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)
⊢ ∀ᶠ (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)
have 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
Tactic: filter_upwards with n z _ using (by simp; abel)
-- 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
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
⊢ 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)
have 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)
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)