awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
m m' : PseudoEMetricSpace α
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
obtain :
  ∀ [toEDist : EDist α] (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x)
    (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (U : UniformSpace α)
    (hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε})
    (h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist),
    { toEDist := toEDist, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
        toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
      m'
⊢ m = m'

Tactic:
obtain ⟨_, _, _, U, hU⟩ := m
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
m' : PseudoEMetricSpace α
ed : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
obtain :
  ∀ [toEDist : EDist α] (edist_self_1 : ∀ (x : α), edist x x = 0) (edist_comm_1 : ∀ (x y : α), edist x y = edist y x)
    (edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) (U' : UniformSpace α)
    (hU' : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε})
    (h : Eq.{u_2 + 1} (α := EDist α) PseudoEMetricSpace.toEDist PseudoEMetricSpace.toEDist),
    { toEDist := ed, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
        toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
      { toEDist := toEDist, edist_self := edist_self_1, edist_comm := edist_comm_1, edist_triangle := edist_triangle_1,
        toUniformSpace := U', uniformity_edist := hU' }
⊢ { toEDist := ed, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
    m'

Tactic:
obtain ⟨_, _, _, U', hU'⟩ := m'
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
ed : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
ed' : EDist α
edist_self_1 : ∀ (x : α), edist x x = 0
edist_comm_1 : ∀ (x y : α), edist x y = edist y x
edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
e_toUniformSpace : U = U'
⊢ { toEDist := ed, edist_self := edist_self, edist_comm := edist_comm, edist_triangle := edist_triangle,
      toUniformSpace := U, uniformity_edist := hU : PseudoEMetricSpace α } =
    { toEDist := ed', edist_self := edist_self_1, edist_comm := edist_comm_1, edist_triangle := edist_triangle_1,
      toUniformSpace := U', uniformity_edist := hU' }

Tactic:
congr 1
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
ed : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
ed' : EDist α
edist_self_1 : ∀ (x : α), edist x x = 0
edist_comm_1 : ∀ (x y : α), edist x y = edist y x
edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
⊢ U = U'

Tactic:
UniformSpace.ext (((show ed = ed' from h) ▸ hU).trans hU'.symm)

Premises used: UniformSpace.ext
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u_2
ed : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
ed' : EDist α
edist_self_1 : ∀ (x : α), edist x x = 0
edist_comm_1 : ∀ (x y : α), edist x y = edist y x
edist_triangle_1 : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
U' : UniformSpace α
hU' : 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}
h : Eq.{u_2 + 1} (α := EDist α) toEDist toEDist
⊢ U = U'

Tactic:
exact UniformSpace.ext (((show ed = ed' from h) ▸ hU).trans hU'.symm)

Premises used: UniformSpace.ext
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
rw : edist x y ≤ edist x z + edist z y
⊢ edist x y ≤ edist z x + edist z y

Tactic:
rw [edist_comm z]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist z y

Tactic:
apply edist_triangle

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
rw : edist x y ≤ edist x z + edist z y
⊢ edist x y ≤ edist x z + edist y z

Tactic:
rw [edist_comm y]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
a : edist x z ≤ edist y z
a₁ : edist y z ≤ edist x z
⊢ edist x z = edist y z

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
a : edist x z ≤ edist x y + edist y z
⊢ edist x z ≤ edist y z

Tactic:
rw [← zero_add (edist y z), ← h]

Premises used: zero_add, EDist.edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist x y + edist y z

Tactic:
apply edist_triangle

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y x = 0

Tactic:
rw [edist_comm] at h

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
a : edist y z ≤ edist y x + edist x z
⊢ edist y z ≤ edist x z

Tactic:
rw [← zero_add (edist x z), ← h]

Premises used: zero_add, EDist.edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist y x + edist x z

Tactic:
apply edist_triangle

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
rw : edist x z = edist y z
⊢ edist z x = edist z y

Tactic:
rw [edist_comm z x, edist_comm z y]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z

Tactic:
apply edist_congr_right h

Premises used: edist_congr_right
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
w x y z : α
hl : edist w x = 0
hr : edist y z = 0
⊢ edist w y = edist x z

Tactic:
(edist_congr_right hl).trans (edist_congr_left hr)

Premises used: edist_congr_left, edist_congr_right, Eq.trans
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y z t : α
grw : edist x z + edist z t ≤ edist x y + edist y z + edist z t
grw₁ : edist x y + edist y z + edist z t ≤ edist x y + edist y z + edist z t
y₁ : α
grw₂ : edist x y + edist y z + edist z t ≤ edist x y + edist y z + edist z t
y₂ : α
⊢ edist x t ≤ edist x y + edist y z + edist z t

Tactic:
grw [edist_triangle _ z, edist_triangle]

Premises used: PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}

Tactic:
PseudoEMetricSpace.uniformity_edist

Premises used: PseudoEMetricSpace.uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ Eq.{u + 1} (α := UniformSpace α) PseudoEMetricSpace.toUniformSpace (uniformSpaceOfEDist edist ⋯ ⋯ ⋯)

Tactic:
UniformSpace.ext uniformity_pseudoedist

Premises used: UniformSpace.ext, uniformity_pseudoedist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ≥0∞) ↦ 0 < ε) fun (ε : ℝ≥0∞) ↦ {p : α × α | edist p.1 p.2 < ε}

Tactic:
(@uniformSpace_edist α _).symm ▸ UniformSpace.hasBasis_ofFun ⟨1, one_pos⟩ _ _ _ _ _

Premises used: UniformSpace.hasBasis_ofFun, Eq.rec, Exists.intro, OfNat.ofNat, Eq.symm, one_pos, uniformSpace_edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s

Tactic:
uniformity_basis_edist.mem_uniformity_iff

Premises used: uniformity_basis_edist, Filter.HasBasis.mem_uniformity_iff, Set.Mem, setOf
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α_1
α : Type u
edist : α → α → ℝ≥0∞
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}

Tactic:
rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : EDist α
edist_self : ∀ (x : α), edist x x = 0
edist_comm : ∀ (x y : α), edist x y = edist y x
edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
⊢ PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle

Tactic:
rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | edist p.1 p.2 < f x}

Tactic:
⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩

Premises used: uniformity_basis_edist, Filter.HasBasis.mem_iff, Filter.HasBasis.mk, Iff.trans
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
refine :
  ∀ (s : Set (α × α)),
    (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | edist p.1 p.2 < f x}

Tactic:
refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
mp :
  (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
mpr :
  (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s
⊢ (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε), ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s

Tactic:
rcases hf ε ε₀ with ⟨i, hi, H⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s

Tactic:
⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩

Premises used: Membership.mem.out, And.intro, Exists.intro, lt_of_lt_of_le
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
i : β
hi : p i
H : f i ≤ ε
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s

Tactic:
fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩

Premises used: setOf, _private.0.EMetric.mk_uniformity_basis.match_1, Exists, HasSubset.Subset, Prod.fst, And, And.intro, LT.lt, Exists.intro, EDist.edist, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s

Tactic:
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | edist p.1 p.2 ≤ f x}

Tactic:
⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩

Premises used: uniformity_basis_edist, Filter.HasBasis.mem_iff, Filter.HasBasis.mk, Iff.trans
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
refine :
  ∀ (s : Set (α × α)),
    (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | edist p.1 p.2 ≤ f x}

Tactic:
refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
mp :
  (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
mpr :
  (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s
⊢ (∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
mp : ∀ (ε' : ℝ≥0∞) (hε' : 0 < ε' ∧ ε' < ε), ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases exists_between ε₀ with ⟨ε', hε'⟩

Premises used: exists_between
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε'), ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
rcases hf ε' hε'.1 with ⟨i, hi, H⟩

Premises used: And.left
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩

Premises used: lt_of_le_of_lt, Membership.mem.out, And.right, And.intro, Exists.intro, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ≥0∞
ε₀ : 0 < ε
hε : {p : α × α | edist p.1 p.2 < ε} ⊆ s
ε' : ℝ≥0∞
hε' : 0 < ε' ∧ ε' < ε
i : β
hi : p i
H : f i ≤ ε'
⊢ ∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s

Tactic:
exact ⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s

Tactic:
fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩

Premises used: Membership.mem.out, setOf, le_of_lt, Exists, HasSubset.Subset, _private.0.EMetric.mk_uniformity_basis_le.match_1, Prod.fst, And, And.intro, LT.lt, Exists.intro, EDist.edist, OfNat.ofNat, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ (i : β), p i ∧ {p : α × α | edist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ≥0∞), 0 < i ∧ {p : α × α | edist p.1 p.2 < i} ⊆ s

Tactic:
exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ≥0∞) ↦ 0 < ε) fun (ε : ℝ≥0∞) ↦ {p : α × α | edist p.1 p.2 ≤ ε}

Tactic:
EMetric.mk_uniformity_basis_le (fun _ => id) fun ε ε₀ => ⟨ε, ε₀, le_refl ε⟩

Premises used: le_refl, EMetric.mk_uniformity_basis_le, id, And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε' : ℝ≥0∞
hε' : 0 < ε'
⊢ (𝓤 α).HasBasis (fun (ε : ℝ≥0∞) ↦ ε ∈ Ioo 0 ε') fun (ε : ℝ≥0∞) ↦ {p : α × α | edist p.1 p.2 < ε}

Tactic:
EMetric.mk_uniformity_basis (fun _ => And.left) fun ε ε₀ =>
    let ⟨δ, hδ⟩ := exists_between hε'
    ⟨min ε δ, ⟨lt_min ε₀ hδ.1, lt_of_le_of_lt (min_le_right _ _) hδ.2⟩, min_le_left _ _⟩

Premises used: lt_of_le_of_lt, Membership.mem, Exists, lt_min, exists_between, LE.le, min_le_left, And, And.right, And.left, And.intro, min_le_right, EMetric.mk_uniformity_basis, Exists.intro, _private.0.uniformity_basis_edist'.match_1, OfNat.ofNat, Set.Ioo, Min.min
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε' : ℝ≥0∞
hε' : 0 < ε'
⊢ (𝓤 α).HasBasis (fun (ε : ℝ≥0∞) ↦ ε ∈ Ioo 0 ε') fun (ε : ℝ≥0∞) ↦ {p : α × α | edist p.1 p.2 ≤ ε}

Tactic:
EMetric.mk_uniformity_basis_le (fun _ => And.left) fun ε ε₀ =>
    let ⟨δ, hδ⟩ := exists_between hε'
    ⟨min ε δ, ⟨lt_min ε₀ hδ.1, lt_of_le_of_lt (min_le_right _ _) hδ.2⟩, min_le_left _ _⟩

Premises used: lt_of_le_of_lt, EMetric.mk_uniformity_basis_le, Membership.mem, Exists, lt_min, exists_between, LE.le, min_le_left, And, And.right, And.left, And.intro, min_le_right, Exists.intro, _private.0.uniformity_basis_edist'.match_1, OfNat.ofNat, Set.Ioo, Min.min
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ≥0) ↦ 0 < ε) fun (ε : ℝ≥0) ↦ {p : α × α | edist p.1 p.2 < (↑ε : ℝ≥0∞)}

Tactic:
EMetric.mk_uniformity_basis (fun _ => ENNReal.coe_pos.2) fun _ε ε₀ =>
    let ⟨δ, hδ⟩ := ENNReal.lt_iff_exists_nnreal_btwn.1 ε₀
    ⟨δ, ENNReal.coe_pos.1 hδ.1, le_of_lt hδ.2⟩

Premises used: Iff.mpr, ENNReal.ofNNReal, le_of_lt, Exists, LE.le, ENNReal.lt_iff_exists_nnreal_btwn, ENNReal.coe_pos, And, And.right, And.left, And.intro, LT.lt, EMetric.mk_uniformity_basis, Exists.intro, Iff.mp, OfNat.ofNat, _private.0.uniformity_basis_edist_nnreal.match_1
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ≥0) ↦ 0 < ε) fun (ε : ℝ≥0) ↦ {p : α × α | edist p.1 p.2 ≤ (↑ε : ℝ≥0∞)}

Tactic:
EMetric.mk_uniformity_basis_le (fun _ => ENNReal.coe_pos.2) fun _ε ε₀ =>
    let ⟨δ, hδ⟩ := ENNReal.lt_iff_exists_nnreal_btwn.1 ε₀
    ⟨δ, ENNReal.coe_pos.1 hδ.1, le_of_lt hδ.2⟩

Premises used: Iff.mpr, ENNReal.ofNNReal, EMetric.mk_uniformity_basis_le, le_of_lt, Exists, LE.le, ENNReal.lt_iff_exists_nnreal_btwn, ENNReal.coe_pos, And, And.right, And.left, And.intro, LT.lt, Exists.intro, Iff.mp, OfNat.ofNat, _private.0.uniformity_basis_edist_nnreal.match_1
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (𝓤 α).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ {p : α × α | edist p.1 p.2 < (↑n : ℝ≥0∞)⁻¹}

Tactic:
EMetric.mk_uniformity_basis (fun n _ ↦ ENNReal.inv_pos.2 <| ENNReal.natCast_ne_top n) fun _ε ε₀ ↦
    let ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt (ne_of_gt ε₀)
    ⟨n, trivial, le_of_lt hn⟩

Premises used: Iff.mpr, trivial, ENNReal.natCast_ne_top, le_of_lt, Exists, ne_of_gt, _private.0.uniformity_basis_edist_inv_nat.match_1, LE.le, Nat.cast, And, Inv.inv, And.intro, True, EMetric.mk_uniformity_basis, Exists.intro, ENNReal.exists_inv_nat_lt, ENNReal.inv_pos
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ (𝓤 α).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ {p : α × α | edist p.1 p.2 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ n}

Tactic:
EMetric.mk_uniformity_basis (fun _ _ ↦ ENNReal.pow_pos (ENNReal.inv_pos.2 ENNReal.ofNat_ne_top) _)
    fun _ε ε₀ ↦
    let ⟨n, hn⟩ := ENNReal.exists_inv_two_pow_lt (ne_of_gt ε₀)
    ⟨n, trivial, le_of_lt hn⟩

Premises used: Iff.mpr, ENNReal.exists_inv_two_pow_lt, ENNReal.ofNat_ne_top, trivial, le_of_lt, Exists, ne_of_gt, LE.le, _private.0.uniformity_basis_edist_inv_two_pow.match_1, And, Inv.inv, HPow.hPow, And.intro, True, EMetric.mk_uniformity_basis, Exists.intro, ENNReal.pow_pos, OfNat.ofNat, ENNReal.inv_pos
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ {p : α × α | edist p.1 p.2 < ε} ∈ 𝓤 α

Tactic:
mem_uniformity_edist.2 ⟨ε, ε0, id⟩

Premises used: Iff.mpr, id, And.intro, Exists.intro, mem_uniformity_edist
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
⊢ (𝓤 α).IsCountablyGenerated

Tactic:
isCountablyGenerated_of_seq ⟨_, uniformity_basis_edist_inv_nat.eq_iInf⟩

Premises used: Filter.isCountablyGenerated_of_seq, uniformity_basis_edist_inv_nat, Filter.HasBasis.eq_iInf, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

Tactic:
uniformity_basis_edist.uniformContinuousOn_iff uniformity_basis_edist

Premises used: uniformity_basis_edist, Set.Mem, setOf, Filter.HasBasis.uniformContinuousOn_iff