awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ s ⊆ t
have st_nonempty : (s ∩ t).Nonempty
Tactic: have st_nonempty : (s ∩ t).Nonempty := ⟨x₀, hx₀, ⟨hx₀, hfg⟩⟩
-- 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
⊢ s ⊆ t
have suffices : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∩ s ⊆ t
Tactic: suffices H : closure t ∩ s ⊆ t from h's.subset_of_closure_inter_subset open_t st_nonempty 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
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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
⊢ x ∈ t
have obtain : ∀ (ε : ℝ) (εpos : ε > 0) (hε : Metric.ball x ε ⊆ s), x ∈ t
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), ε > 0 ∧ Metric.ball x ε ⊆ s := Metric.isOpen_iff.1 hs x xs
-- 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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ x ∈ t
have obtain : ∀ (y : E) (yt : y ∈ t) (hxy : dist x y < ε / 2), x ∈ t
Tactic: obtain ⟨y, yt, hxy⟩ : ∃ (y : E), y ∈ t ∧ dist x y < ε / 2 :=
    Metric.mem_closure_iff.1 xt _ (half_pos εpos)
-- 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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ Metric.ball y (ε / 2) ⊆ Metric.ball x ε
have h : ε / 2 + dist y x ≤ ε
Tactic: apply Metric.ball_subset_ball'
-- 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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist y x ≤ ε
have h : ε / 2 + dist x y ≤ ε
Tactic: rw [dist_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
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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist x y ≤ ε
have linarith : ε < ε / 2 + dist x y → 2 / 2 = 1
Tactic: linarith
-- 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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
linarith : ε < ε / 2 + dist x y → 2 / 2 = 1
⊢ ε / 2 + dist x y ≤ ε
have linarith₁ : ε < ε / 2 + dist x y → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
linarith : ε < ε / 2 + dist x y → 2 / 2 = 1
linarith₁ : ε < ε / 2 + dist x y → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ε / 2 + dist x y ≤ ε
have linarith₂ : ε < ε / 2 + dist x y → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
linarith : ε < ε / 2 + dist x y → 2 / 2 = 1
linarith₁ : ε < ε / 2 + dist x y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε < ε / 2 + dist x y → GT.gt (α := ℝ) 2 0
linarith₃ : ε < ε / 2 + dist x y → 2 / 2 = 1
linarith₄ : ε < ε / 2 + dist x y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ε < ε / 2 + dist x y → GT.gt (α := ℝ) 2 0
⊢ ε / 2 + dist x y ≤ ε
have linarith₆ : ε < ε / 2 + dist x y → 2 * dist x y - 1 * ε + (2 * ε - (1 * ε + 2 * dist x y)) = 0
Tactic: linarith
-- 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_1 : E
hx₀ : x₀ ∈ s
hx : 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
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ x ∈ t
have B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
Tactic: have B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε := by
    apply Metric.ball_subset_ball'; rw [dist_comm]; linarith
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
⊢ 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)
have 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)
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 _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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.{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)
have 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)
Tactic: rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
⊢ 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)
have 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)) <
      ε
Tactic: rw [Metric.tendstoUniformlyOnFilter_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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
⊢ ∀ ε > 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)) <
        ε
have hfg' : UniformCauchySeqOnFilter f' l (𝓝 x)
Tactic: have hfg' := hf'.uniformCauchySeqOnFilter
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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)
⊢ ∀ ε > 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)) <
        ε
have hfg'₁ : 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'
Cleared hypotheses: hfg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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)
          (-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)) <
        ε
have 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) < ε
Tactic: rw [Metric.tendstoUniformlyOnFilter_iff] at hfg'
Cleared hypotheses: hfg'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (goal)
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
⊢ ∀ᶠ (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)) <
      ε
have 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)) <
      ε
Tactic: obtain ⟨q, hqpos, hqε⟩ := exists_pos_rat_lt hε
-- Lean 4 proof step from Mathlib.Analysis.Calculus.UniformLimitsDeriv (hypothesis)
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)
        (-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)) <
      ε
have 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 : ℝ)
Tactic: specialize hfg' (q : ℝ) (by simp [hqpos])
Cleared hypotheses: hfg'