awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
rw :
  IsUniformInducing f ∧ Function.Injective f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
rw₁ :
  Function.Injective f ∧ IsUniformInducing f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
rw₂ rw₃ :
  (Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ) ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff]

Premises used: Metric.isUniformInducing_iff, and_comm, Metric.isUniformEmbedding_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : IsUniformInducing f
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
⟨uniformContinuous_iff.1 h.uniformContinuous, (isUniformInducing_iff.1 h).2⟩

Premises used: Metric.isUniformInducing_iff, And.right, And.intro, Iff.mp, Metric.uniformContinuous_iff, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : IsUniformEmbedding f
⊢ (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε) ∧
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
controlled_of_isUniformInducing h.toIsUniformInducing

Premises used: Metric.controlled_of_isUniformInducing, IsUniformEmbedding.toIsUniformInducing
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ TotallyBounded s ↔ ∀ ε > 0, ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
uniformity_basis_dist.totallyBounded_iff

Premises used: Set.Mem, setOf, Metric.uniformity_basis_dist, Metric.ball, Filter.HasBasis.totallyBounded_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
inl : ∀ (hs : s = ∅), TotallyBounded s
inr : ∀ (hs : s.Nonempty), TotallyBounded s
⊢ TotallyBounded s

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
hs : s = ∅
inl : TotallyBounded.{u} (α := α) ∅
⊢ TotallyBounded s

Tactic:
rw [hs]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
hs : s = ∅
⊢ TotallyBounded.{u} (α := α) ∅

Tactic:
totallyBounded_empty

Premises used: totallyBounded_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
hs : s = ∅
⊢ TotallyBounded.{u} (α := α) ∅

Tactic:
exact totallyBounded_empty

Premises used: totallyBounded_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
hs : s.Nonempty
inr : ∀ (x0 : α) (hx0 : x0 ∈ s), TotallyBounded s
⊢ TotallyBounded s

Tactic:
rcases hs with ⟨x0, hx0⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
inr : ∀ (this : Inhabited (↑s : Type u)), TotallyBounded s
⊢ TotallyBounded s

Tactic:
haveI : Inhabited s := ⟨⟨x0, hx0⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
⊢ TotallyBounded s

Tactic:
totallyBounded_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, Metric.totallyBounded_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
inr : ∀ (ε : ℝ) (ε0 : ε > 0), ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
⊢ TotallyBounded s

Tactic:
refine totallyBounded_iff.2 fun ε ε0 => ?_

Premises used: Iff.mpr, Metric.totallyBounded_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
inr :
  ∀ (β : Type u) (fβ : Fintype β) (F : (↑s : Type u) → β)
    (hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε),
    ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rcases H ε ε0 with ⟨β, fβ, F, hF⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩

Premises used: Function.comp, Set.finite_range, And.intro, Exists.intro, Set.range, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
inr :
  ∀ (x : α) (xs : x ∈ s),
    Membership.mem (γ := Set α) (⋃ y ∈ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv), ball y ε) x
⊢ ∃ (t : Set α), t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
x : α
xs : x ∈ s
x' : (↑s : Type u) := Finv (F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs))
⊢ F x' = F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs)

Tactic:
have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this_1 : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
x : α
xs : x ∈ s
x' : (↑s : Type u) := Finv (F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs))
this : F x' = F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs)
inr : ∃ (i : α) (_ : ∃ (y : β), (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv) y = i), x ∈ ball i ε
⊢ Membership.mem (γ := Set α) (⋃ y ∈ range (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv), ball y ε) x

Tactic:
simp only [Set.mem_iUnion, Set.mem_range]

Premises used: Set.mem_range, Set.mem_iUnion
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this_1 : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
x : α
xs : x ∈ s
x' : (↑s : Type u) := Finv (F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs))
this : F x' = F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs)
⊢ ∃ (i : α) (_ : ∃ (y : β), (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv) y = i), x ∈ ball i ε

Tactic:
⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩

Premises used: Subtype.mk, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
H :
  ∀ ε > 0,
    ∃ (β : Type u) (x : Fintype β) (F : (↑s : Type u) → β),
      ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
x0 : α
hx0 : x0 ∈ s
this_1 : Inhabited (↑s : Type u)
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : (↑s : Type u) → β
hF : ∀ (x y : (↑s : Type u)), F x = F y → dist (↑x : α) (↑y : α) < ε
Finv : β → (↑s : Type u) := Function.invFun F
x : α
xs : x ∈ s
x' : (↑s : Type u) := Finv (F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs))
this : F x' = F (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x xs)
⊢ ∃ (i : α) (_ : ∃ (y : β), (Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ Finv) y = i), x ∈ ball i ε

Tactic:
exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : TotallyBounded s
ε : ℝ
ε_pos : ε > 0
rw :
  ∀ (hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}) (ε : ℝ) (ε_pos : ε > 0),
    ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
rw [totallyBounded_iff_subset] at hs

Premises used: totallyBounded_iff_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
hs _ (dist_mem_uniformity ε_pos)

Premises used: Set.Mem, setOf, Metric.ball, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
exact hs _ (dist_mem_uniformity ε_pos)

Premises used: Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
⊢ TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε

Tactic:
⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩

Premises used: setOf, Prod.fst, LT.lt, Iff.intro, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
refine :
  ∀ (H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε) (u : Set (α × α)) (hu : u ∈ 𝓤 α),
    ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
⊢ TendstoUniformlyOnFilter F f p p' ↔ ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
rcases :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u),
    ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
(H ε εpos).mono fun n hn => hε hn

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
p' : Filter β
H : ∀ ε > 0, ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.2) (F n.1 n.2) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι × β) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

Tactic:
exact (H ε εpos).mono fun n hn => hε hn

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩

Premises used: setOf, Prod.fst, LT.lt, Iff.intro, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
refine :
  ∀ (H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε) (u : Set (α × α))
    (hu : u ∈ 𝓤 α) (x : β) (hx : x ∈ s), ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ TendstoLocallyUniformlyOn F f p s ↔ ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu x hx => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
rcases :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u),
    ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
rcases :
  ∀ (t : Set β) (ht : t ∈ 𝓝[s] x) (Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε),
    ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases H ε εpos x hx with ⟨t, ht, Ht⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩

Premises used: Filter.Eventually.mono, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
t : Set β
ht : t ∈ 𝓝[s] x
Ht : ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨t, ht, Ht.mono fun n hs x hx => hε (hs x hx)⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε

Tactic:
⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩

Premises used: setOf, Prod.fst, LT.lt, Iff.intro, Dist.dist, Prod.snd, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
refine :
  ∀ (H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε) (u : Set (α × α)) (hu : u ∈ 𝓤 α),
    ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε

Tactic:
refine ⟨fun H ε hε => H _ (dist_mem_uniformity hε), fun H u hu => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
rcases :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u), ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
(H ε εpos).mono fun n hs x hx => hε (hs x hx)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, dist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ
εpos : ε > 0
hε : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

Tactic:
exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε

Tactic:
simp only [← tendstoLocallyUniformlyOn_univ, tendstoLocallyUniformlyOn_iff, nhdsWithin_univ,
    mem_univ, forall_const]

Premises used: nhdsWithin_univ, Metric.tendstoLocallyUniformlyOn_iff, Set.mem_univ, forall_const, tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
rw :
  (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), Membership.mem (γ := Set β) univ x → dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff]

Premises used: tendstoUniformlyOn_univ, Metric.tendstoUniformlyOn_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
ι : Type u_1
inst : PseudoMetricSpace α
F : ι → β → α
f : β → α
p : Filter ι
⊢ (∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), Membership.mem (γ := Set β) univ x → dist (f x) (F n x) < ε) ↔
    ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε

Tactic:
uniformity_basis_dist.cauchy_iff

Premises used: Set.Mem, Metric.uniformity_basis_dist, Filter.HasBasis.cauchy_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : IsDiscrete s
x : α
hx : x ∈ s
⊢ ∃ ε > 0, ball x ε ∩ s = {x}

Tactic:
nhds_basis_ball.exists_inter_eq_singleton_of_mem_discrete hs hx

Premises used: Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : IsDiscrete s
x : α
hx : x ∈ s
⊢ ∃ ε > 0, closedBall x ε ∩ s = {x}

Tactic:
nhds_basis_closedBall.exists_inter_eq_singleton_of_mem_discrete hs hx

Premises used: Filter.HasBasis.exists_inter_eq_singleton_of_mem_discrete, Metric.nhds_basis_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : edist x y = 0 ↔ nndist x y = 0
rw₁ : (↑(nndist x y) : ℝ≥0∞) = 0 ↔ nndist x y = 0
rw₂ rw₃ : nndist x y = 0 ↔ nndist x y = 0
⊢ Inseparable x y ↔ nndist x y = 0

Tactic:
rw [EMetric.inseparable_iff, edist_nndist, ENNReal.coe_eq_zero]

Premises used: ENNReal.coe_eq_zero, edist_nndist, EMetric.inseparable_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : nndist x y = 0 ↔ dist x y = 0
rw₁ : nndist x y = 0 ↔ (↑(nndist x y) : ℝ) = 0
rw₂ rw₃ : nndist x y = 0 ↔ nndist x y = 0
⊢ Inseparable x y ↔ dist x y = 0

Tactic:
rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]

Premises used: NNReal.coe_eq_zero, dist_nndist, Metric.inseparable_iff_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Basic
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
l : Filter β
x y : α
inst_1 : l.NeBot
ha : Tendsto f l (𝓝 x)
hb : Tendsto f l (𝓝 y)
⊢ dist x y = 0

Tactic:
(tendsto_nhds_unique_inseparable ha hb).dist_eq_zero

Premises used: Inseparable.dist_eq_zero, tendsto_nhds_unique_inseparable