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
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 - (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)
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)
Tactic: constructor
-- 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
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 : ι × ι) (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)
have 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)
Tactic: constructor
-- 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 - (f n.1 x - f n.2 x)) 0
    (l ×ˢ l) (Metric.ball x r)
have 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)) < ε
Tactic: rw [Metric.tendstoUniformlyOn_iff] at hf' ⊢
Cleared hypotheses: hf', this_2, this, 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 : ∀ (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
⊢ ∃ (q : ℝ), 0 < q ∧ q * r < ε
have simp_rw : ∃ (q : ℝ), 0 < q ∧ r * q < ε
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
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
⊢ ∀ᶠ (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)) < ε
have inr : ∀ (q : ℝ) (hqpos : 0 < q) (hq : q * r < ε),
  ∀ᶠ (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)) < ε
Tactic: obtain ⟨q, hqpos, hq⟩ : ∃ q : ℝ, 0 < q ∧ q * r < ε := by
      simp_rw [mul_comm]
      exact exists_pos_mul_lt hε.lt r
-- 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' : ∀ ε > 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
q : ℝ
hqpos : 0 < q
hq : q * r < ε
⊢ ∀ᶠ (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)) < ε
have inr : ∀ (x_1 : ι × ι),
  (∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (-f' x_1.1 x_2 + f' x_1.2 x_2) < q) →
    ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f x_1.1 x_2 - f x_1.2 x_2 - (f x_1.1 x - f x_1.2 x)) < ε
Tactic: apply (hf' q hqpos.gt).mono
-- 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' : ∀ ε > 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
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
hn : ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < q
y : E
hy : y ∈ Metric.ball x r
⊢ dist (0 y) (f n.1 y - f n.2 y - (f n.1 x - f n.2 x)) < ε
have inr : ∀ (hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q), ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε
Tactic: simp_rw [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg, norm_neg_add] at hn ⊢
Cleared hypotheses: hn
-- 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' : ∀ ε > 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
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε
have mvt : ‖(f n.1 - f n.2) y - (f n.1 - f n.2) x‖ ≤ q * ‖y - x‖
Tactic: have mvt :=
      Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
        (fun z hz => ((hf n.1 z hz).sub (hf n.2 z hz)).hasFDerivWithinAt) (fun z hz => (hn z hz).le)
        (convex_ball x r) (Metric.mem_ball_self hr) 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
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
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
mvt : ‖(f n.1 - f n.2) y - (f n.1 - f n.2) x‖ ≤ q * ‖y - x‖
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε
have inr : q * ‖y - x‖ < ε
Tactic: refine lt_of_le_of_lt mvt ?_
-- 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' : ∀ ε > 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
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
mvt : ‖(f n.1 - f n.2) y - (f n.1 - f n.2) x‖ ≤ q * ‖y - x‖
⊢ q * ‖y - x‖ < ε
have this₁ : q * ‖y - x‖ < q * r
Tactic: have : q * ‖y - x‖ < q * r :=
      mul_lt_mul' rfl.le (by simpa only [dist_eq_norm] using Metric.mem_ball.mp hy) (norm_nonneg _)
        hqpos
-- 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 : ι × ι) (x_1 : E) ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
have inr : ∀ (ε : ℝ) (hε : ε > 0), ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x - f n.2 x) < ε
Tactic: refine Metric.tendstoUniformlyOn_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
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
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x - f n.2 x) < ε
have inr : ∀ (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 : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x - f n.2 x) < ε
Tactic: obtain ⟨t, ht, ht'⟩ := (Metric.cauchy_iff.mp hfg).2 ε 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
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
ε : ℝ
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 : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x - f n.2 x) < ε
have inr : ∃ (pa : ι → Prop),
  (∀ᶠ (x : ι) in l, pa x) ∧
    ∃ (pb : ι → Prop),
      (∀ᶠ (y : ι) in l, pb y) ∧
        ∀ {x_1 : ι},
          pa x_1 → ∀ {y : ι}, pb y → ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f (x_1, y).1 x - f (x_1, y).2 x) < ε
Tactic: rw [eventually_prod_iff]
-- 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
ε : ℝ
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 < ε
⊢ ∃ (pa : ι → Prop),
    (∀ᶠ (x : ι) in l, pa x) ∧
      ∃ (pb : ι → Prop),
        (∀ᶠ (y : ι) in l, pb y) ∧
          ∀ {x_1 : ι},
            pa x_1 → ∀ {y : ι}, pb y → ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f (x_1, y).1 x - f (x_1, y).2 x) < ε
have inr : ∀ {x_1 : ι},
  (fun (n : ι) ↦ f n x ∈ t) x_1 →
    ∀ {y : ι}, (fun (n : ι) ↦ f n x ∈ t) y → ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f (x_1, y).1 x - f (x_1, y).2 x) < ε
Tactic: refine ⟨fun n => f n x ∈ t, ht, fun n => f n x ∈ t, ht, ?_⟩
-- 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
ε : ℝ
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 : ι
hn : f n x ∈ t
n' : ι
hn' : f n' x ∈ t
z : E
h : z ∈ Metric.ball x r
⊢ dist (0 z) (f (n, n').1 x - f (n, n').2 x) < ε
have inr : dist (f (n, n').1 x) (f (n, n').2 x) < ε
Tactic: rw [dist_eq_norm, Pi.zero_apply, zero_sub, norm_neg, ← dist_eq_norm]
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x₀) l)
⊢ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y : E | y ∈ s ∧ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n y) l)}
⊢ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)
have suffices : s ⊆ t
Tactic: suffices H : s ⊆ t from (H hx).2
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y : E | y ∈ s ∧ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n y) l)}
⊢ s ⊆ t
have A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
Tactic: have A : ∀ x ε, x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t := fun x ε xt hx y hy =>
    ⟨hx hy,
      (uniformCauchySeqOn_ball_of_fderiv (hf'.mono hx) (fun n y hy => hf n y (hx hy))
            xt.2).cauchy_map
        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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y : E | y ∈ s ∧ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
have rw : ∀ x ∈ t, ∃ ε > 0, Metric.ball x ε ⊆ t
Tactic: rw [Metric.isOpen_iff]
-- 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x_1 : E
hx₀ : x₀ ∈ s
hx_1 : x_1 ∈ s
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y : E | y ∈ s ∧ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
x : E
hx : x ∈ t
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t
have rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : Metric.ball x ε ⊆ s), ∃ ε > 0, Metric.ball x ε ⊆ t
Tactic: rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, 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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y : E | y ∈ s ∧ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
⊢ s ⊆ t
have open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
Tactic: have open_t : IsOpen t := by
    rw [Metric.isOpen_iff]
    intro x hx
    rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, hε⟩
    exact ⟨ε, εpos, A x ε hx hε⟩