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
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)
⊢ 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
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)}
suffices : s ⊆ t
⊢ Cauchy.{u_4} (α := G) (map (fun (n : ι) ↦ f n x) l)

Tactic:
suffices H : s ⊆ t from (H hx).2
-- 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
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)}
⊢ ∀ (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⟩
-- 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
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
rw : ∀ x ∈ t, ∃ ε > 0, Metric.ball x ε ⊆ t
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t

Tactic:
rw [Metric.isOpen_iff]

Premises used: Metric.isOpen_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
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
rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : Metric.ball x ε ⊆ s), ∃ ε > 0, Metric.ball x ε ⊆ t
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
rcases Metric.isOpen_iff.1 hs x hx.1 with ⟨ε, εpos, hε⟩

Premises used: Metric.isOpen_iff, And.left, Iff.mp
-- 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
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
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
⟨ε, εpos, A x ε hx hε⟩

Premises used: And.intro, Exists.intro
-- 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
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
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
⊢ ∃ ε > 0, Metric.ball x ε ⊆ t

Tactic:
exact ⟨ε, εpos, A x ε hx hε⟩
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
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

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ε⟩
-- 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
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).Nonempty

Tactic:
have st_nonempty : (s ∩ t).Nonempty := ⟨x₀, hx₀, ⟨hx₀, hfg⟩⟩
-- 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
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
suffices : closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∩ s ⊆ t
⊢ s ⊆ t

Tactic:
suffices H : closure t ∩ s ⊆ t from h's.subset_of_closure_inter_subset open_t st_nonempty H
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : NontriviallyNormedField 𝕜
inst_2 : IsRCLikeNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
G : Type u_4
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace 𝕜 G
f : ι → E → G
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
⊢ ∃ ε > 0, Metric.ball x ε ⊆ s

Tactic:
Metric.isOpen_iff.1 hs x xs

Premises used: Metric.isOpen_iff, Iff.mp
-- 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
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
obtain : ∀ (ε : ℝ) (εpos : ε > 0) (hε : Metric.ball x ε ⊆ s), x ∈ t
⊢ x ∈ t

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), ε > 0 ∧ Metric.ball x ε ⊆ s := Metric.isOpen_iff.1 hs x xs

Premises used: Metric.isOpen_iff, Iff.mp
-- 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
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 ∈ t, dist x y < ε / 2

Tactic:
Metric.mem_closure_iff.1 xt _ (half_pos εpos)

Premises used: half_pos, Metric.mem_closure_iff, Iff.mp
-- 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
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
obtain : ∀ (y : E) (yt : y ∈ t) (hxy : dist x y < ε / 2), x ∈ t
⊢ x ∈ t

Tactic:
obtain ⟨y, yt, hxy⟩ : ∃ (y : E), y ∈ t ∧ dist x y < ε / 2 :=
    Metric.mem_closure_iff.1 xt _ (half_pos εpos)

Premises used: half_pos, Metric.mem_closure_iff, Iff.mp
-- 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
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
h : ε / 2 + dist y x ≤ ε
⊢ Metric.ball y (ε / 2) ⊆ Metric.ball x ε

Tactic:
apply Metric.ball_subset_ball'

Premises used: Metric.ball_subset_ball'
-- 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
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
h : ε / 2 + dist x y ≤ ε
⊢ ε / 2 + dist y x ≤ ε

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- 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
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
linarith₆ : ε < ε / 2 + dist x y → 2 * dist x y - 1 * ε + (2 * ε - (1 * ε + 2 * dist x y)) = 0
⊢ ε / 2 + dist x y ≤ ε

Tactic:
linarith
-- 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
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 ε

Tactic:
have B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε := by
    apply Metric.ball_subset_ball'; rw [dist_comm]; linarith
-- 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
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
B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
⊢ x ∈ t

Tactic:
A y (ε / 2) yt (B.trans hε) (Metric.mem_ball.2 hxy)

Premises used: Iff.mpr, HasSubset.Subset.trans, HDiv.hDiv, Metric.mem_ball, 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
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
B : Metric.ball y (ε / 2) ⊆ Metric.ball x ε
⊢ x ∈ t

Tactic:
exact A y (ε / 2) yt (B.trans hε) (Metric.mem_ball.2 hxy)

Premises used: Iff.mpr, HasSubset.Subset.trans, HDiv.hDiv, Metric.mem_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv
Goal:
ι : Type u_1
l : Filter ι
E : Type u_5
inst : NormedAddCommGroup E
𝕜 : Type u_6
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
G : Type u_7
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt.{u_6, u_5, u_7} (𝕜 := 𝕜) (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun (n : ι) ↦ f n y) l (𝓝 (g y))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ TendstoUniformlyOnFilter.{u_5, u_7, u_1} (β := G)
    (fun (n : ι) (y : E) ↦ HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (f n y - f n x))
    (fun (y : E) ↦ HSMul.hSMul.{u_6, u_7, u_7} (α := 𝕜) (↑‖y - x‖ : 𝕜)⁻¹ (g y - g x)) l (𝓝 x)

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

Premises used: Iff.mpr, Norm.norm, Filter.Eventually.self_of_nhds, HSub.hSub, Filter.Eventually.and, RCLike.ofReal, UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto, Filter.Eventually.mono, Filter.Tendsto.const_smul, Inv.inv, And.right, And.left, Filter.eventually_const, Filter.Tendsto.sub