awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε

Tactic:
uniformity_basis_edist.uniformContinuous_iff uniformity_basis_edist

Premises used: uniformity_basis_edist, Set.Mem, setOf, Filter.HasBasis.uniformContinuous_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
p : α → Prop
x y : Subtype p
⊢ edist x y = edist (↑x : α) (↑y : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
p : α → Prop
x y : α
hx : p x
hy : p y
⊢ edist (mk (p := p) x hx) (mk (p := p) y hy) = edist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : αᵐᵒᵖ
⊢ edist (unop x) (unop y) = edist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ edist (op x) (op y) = edist x y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : ULift.{u_2, u} α
⊢ edist x y = edist x.down y.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
⊢ edist { down := x : ULift.{u_2, u} α } { down := y : ULift.{u_2, u} α } = edist x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x : α × β
⊢ max (edist x.1 x.1) (edist x.2 x.2) = 0

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : α × β
⊢ max (edist x.1 y.1) (edist x.2 y.2) = max (edist y.1 x.1) (edist y.2 x.2)

Tactic:
simp [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := Filter ((α × β) × α × β))
    (comap (fun (p : (α × β) × α × β) ↦ (p.1.1, p.2.1)) (𝓤 α) ⊓
      comap (fun (p : (α × β) × α × β) ↦ (p.1.2, p.2.2)) (𝓤 β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α × β) × α × β | max (edist p.1.1 p.2.1) (edist p.1.2 p.2.2) < ε})

Tactic:
simp [PseudoEMetricSpace.uniformity_edist, ← iInf_inf_eq, setOf_and]

Premises used: Set.setOf_and, PseudoEMetricSpace.uniformity_edist, iInf_inf_eq
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
x y : α × β
⊢ edist x y = max (edist x.1 y.1) (edist x.2 y.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : y ∈ eball x ε ↔ edist y x < ε
rw₁ rw₂ : edist y x < ε ↔ edist y x < ε
⊢ y ∈ eball x ε ↔ edist x y < ε

Tactic:
rw [edist_comm, mem_eball]

Premises used: PseudoEMetricSpace.edist_comm, Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist y x ≤ ε

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : y ∈ closedEBall x ε ↔ edist y x ≤ ε
rw₁ rw₂ : edist y x ≤ ε ↔ edist y x ≤ ε
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε

Tactic:
rw [edist_comm, mem_closedEBall]

Premises used: PseudoEMetricSpace.edist_comm, Metric.mem_closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ closedEBall x ∞ = univ

Tactic:
eq_univ_of_forall fun _ => mem_setOf.2 le_top

Premises used: Iff.mpr, Set.mem_setOf, Set.eq_univ_of_forall, le_top
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ eball x ε ⊆ closedEBall x ε

Tactic:
fun _ h => le_of_lt h.out

Premises used: Membership.mem.out, Set.Mem, setOf, le_of_lt, Set.Subset, Metric.closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
hy : y ∈ eball x ε
⊢ 0 < ε

Tactic:
hy.pos

Premises used: LT.lt.pos
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
h : 0 < ε
rwa : edist x x < ε
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < ε
⊢ x ∈ eball x ε

Tactic:
rwa [mem_eball, edist_self]

Premises used: PseudoEMetricSpace.edist_self, Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
rw : 0 ≤ ε
⊢ x ∈ closedEBall x ε

Tactic:
rw [mem_closedEBall, edist_self]

Premises used: Metric.mem_closedEBall, PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ 0 ≤ ε

Tactic:
apply zero_le

Premises used: zero_le
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : edist y x < ε ↔ y ∈ eball x ε
rw₁ rw₂ : edist y x < ε ↔ edist y x < ε
⊢ x ∈ eball y ε ↔ y ∈ eball x ε

Tactic:
rw [mem_eball', mem_eball]

Premises used: Metric.mem_eball', Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
rw : edist y x ≤ ε ↔ y ∈ closedEBall x ε
rw₁ rw₂ : edist y x ≤ ε ↔ edist y x ≤ ε
⊢ x ∈ closedEBall y ε ↔ y ∈ closedEBall x ε

Tactic:
rw [mem_closedEBall', mem_closedEBall]

Premises used: Metric.mem_closedEBall, Metric.mem_closedEBall'
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε₁ ε₂ : ℝ≥0∞
h : ε₁ ≤ ε₂
⊢ eball x ε₁ ⊆ eball x ε₂

Tactic:
fun _y (yx : _ < ε₁) =>
  lt_of_lt_of_le yx h

Premises used: Set.Mem, setOf, Metric.eball, Set.Subset, lt_of_lt_of_le
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε₁ ε₂ : ℝ≥0∞
h : ε₁ ≤ ε₂
⊢ closedEBall x ε₁ ⊆ closedEBall x ε₂

Tactic:
fun _y (yx : _ ≤ ε₁) => le_trans yx h

Premises used: Set.Mem, setOf, Set.Subset, Metric.closedEBall, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε₁ ε₂ : ℝ≥0∞
h : ε₁ + ε₂ ≤ edist x y
⊢ Disjoint (eball x ε₁) (eball y ε₂)

Tactic:
Set.disjoint_left.mpr fun z h₁ h₂ =>
    (edist_triangle_left x y z).not_gt <| (ENNReal.add_lt_add h₁ h₂).trans_le h

Premises used: Iff.mpr, Set.disjoint_left, LE.le.not_gt, LT.lt.trans_le, edist_triangle_left, ENNReal.add_lt_add
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε₁ ε₂ : ℝ≥0∞
h : edist x y + ε₁ ≤ ε₂
h' : edist x y ≠ ∞
⊢ eball x ε₁ ⊆ eball y ε₂

Tactic:
fun z zx =>
  calc
    edist z y ≤ edist z x + edist x y := edist_triangle _ _ _
    _ = edist x y + edist z x := add_comm _ _
    _ < edist x y + ε₁ := ENNReal.add_lt_add_left h' zx
    _ ≤ ε₂ := h

Premises used: Trans.trans, ENNReal.add_lt_add_left, Set.Mem, setOf, Metric.eball, Set.Subset, add_comm, EDist.edist, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ 0 < ε - edist y x

Tactic:
simpa using h
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ 0 < ε - edist y x

Tactic:
have : 0 < ε - edist y x := by simpa using h
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε

Tactic:
⟨ε - edist y x, this, eball_subset ?_ (ne_top_of_lt h)⟩

Premises used: HSub.hSub, Metric.eball_subset, And.intro, Exists.intro, EDist.edist, ne_top_of_lt
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
refine : edist y x + (ε - edist y x) ≤ ε
⊢ ∃ ε' > 0, eball y ε' ⊆ eball x ε

Tactic:
refine ⟨ε - edist y x, this, eball_subset ?_ (ne_top_of_lt h)⟩
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε

Tactic:
(add_tsub_cancel_of_le (mem_eball.mp h).le).le

Premises used: LT.lt.le, Eq.le, Iff.mp, add_tsub_cancel_of_le, Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε

Tactic:
exact (add_tsub_cancel_of_le (mem_eball.mp h).le).le

Premises used: LT.lt.le, Eq.le, Iff.mp, add_tsub_cancel_of_le, Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ eball x ε = ∅ ↔ ε = 0

Tactic:
eq_empty_iff_forall_notMem.trans
    ⟨fun h => le_bot_iff.1 (le_of_not_gt fun ε0 => h _ (mem_eball_self ε0)), fun ε0 _ h =>
      not_lt_of_ge (le_of_eq ε0) (pos_of_mem_eball h)⟩

Premises used: le_bot_iff, le_of_not_gt, Set.eq_empty_iff_forall_notMem, Metric.pos_of_mem_eball, Iff.intro, Iff.mp, Iff.trans, le_of_eq, Metric.mem_eball_self, not_lt_of_ge
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ OrdConnected (α := ℝ≥0∞) {r : ℝ≥0∞ | closedEBall x r ⊆ s}

Tactic:
⟨fun _ _ _ h₁ _ h₂ => (closedEBall_subset_closedEBall h₂.2).trans h₁⟩

Premises used: HasSubset.Subset.trans, Set.OrdConnected.mk, And.right, Metric.closedEBall_subset_closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ OrdConnected (α := ℝ≥0∞) {r : ℝ≥0∞ | eball x r ⊆ s}

Tactic:
⟨fun _ _ _ h₁ _ h₂ => (eball_subset_eball h₂.2).trans h₁⟩

Premises used: Metric.eball_subset_eball, HasSubset.Subset.trans, Set.OrdConnected.mk, And.right
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
rw : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ edist x x < ∞

Tactic:
rw [edist_self]

Premises used: PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x_1 y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x : α
⊢ LT.lt (α := ℝ≥0∞) 0 ∞

Tactic:
exact ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
inst : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
x_1 y_1 : α
h rwa rwa₁ rwa₂ rwa₃ : edist x_1 y_1 < ∞
⊢ edist y_1 x_1 < ∞

Tactic:
rwa [edist_comm]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
rw rw₁ : Eq (α := ℝ≥0∞) 0 0
⊢ eball x 0 = ∅

Tactic:
rw [eball_eq_empty_iff]

Premises used: Metric.eball_eq_empty_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (ε : ℝ≥0∞) ↦ 0 < ε) (eball x)

Tactic:
nhds_basis_uniformity uniformity_basis_edist

Premises used: uniformity_basis_edist, Set.Mem, setOf, Metric.eball, nhds_basis_uniformity
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ (𝓝[s] x).HasBasis (fun (ε : ℝ≥0∞) ↦ 0 < ε) fun (ε : ℝ≥0∞) ↦ eball x ε ∩ s

Tactic:
nhdsWithin_hasBasis nhds_basis_eball s

Premises used: Metric.nhds_basis_eball, nhdsWithin_hasBasis
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (ε : ℝ≥0∞) ↦ 0 < ε) (closedEBall x)

Tactic:
nhds_basis_uniformity uniformity_basis_edist_le

Premises used: Set.Mem, uniformity_basis_edist_le, setOf, Metric.closedEBall, nhds_basis_uniformity
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ (𝓝[s] x).HasBasis (fun (ε : ℝ≥0∞) ↦ 0 < ε) fun (ε : ℝ≥0∞) ↦ closedEBall x ε ∩ s

Tactic:
nhdsWithin_hasBasis nhds_basis_closedEBall s

Premises used: nhdsWithin_hasBasis, Metric.nhds_basis_closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ 𝓝 x = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 (eball x ε)

Tactic:
nhds_basis_eball.eq_biInf

Premises used: Filter.HasBasis.eq_biInf, Metric.nhds_basis_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ ε > 0, eball x ε ⊆ s

Tactic:
nhds_basis_eball.mem_iff

Premises used: Filter.HasBasis.mem_iff, Metric.nhds_basis_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s t : Set α
⊢ s ∈ 𝓝[t] x ↔ ∃ ε > 0, eball x ε ∩ t ⊆ s

Tactic:
nhdsWithin_basis_eball.mem_iff

Premises used: Metric.nhdsWithin_basis_eball, Filter.HasBasis.mem_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, eball x ε ⊆ s

Tactic:
simp [isOpen_iff_nhds, mem_nhds_iff]

Premises used: EMetric.mem_nhds_iff, isOpen_iff_nhds
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
s : Set α
⊢ (∀ (i : ℝ≥0∞), 0 < i → ∃ y ∈ s, y ∈ eball x i) ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

Tactic:
simp only [mem_eball, edist_comm x]

Premises used: PseudoEMetricSpace.edist_comm, Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
x : α
⊢ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ r > 0, (eball x r ∩ s).Nonempty

Tactic:
simp only [mem_closure_iff, Set.Nonempty, mem_inter_iff, and_comm, mem_eball']

Premises used: Set.mem_inter_iff, and_comm, Set.Nonempty, EMetric.mem_closure_iff, Metric.mem_eball'
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, edist (u x) a < ε

Tactic:
nhds_basis_eball.tendsto_right_iff

Premises used: Set.Mem, setOf, Metric.eball, Metric.nhds_basis_eball, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia, u x ∈ eball a ib) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, edist (u n) a < ε

Tactic:
simp only [true_and, mem_Ici, mem_eball]

Premises used: Set.mem_Ici, true_and, Metric.mem_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
simp : edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
⊢ x ∈ eball a δ ∩ s → f x ∈ eball b ε ∩ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
t : Set β
a : α
b : β
ε : ℝ≥0∞
h : 0 < ε
δ : ℝ≥0∞
h_1 : 0 < δ
x : α
mp : (edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr : (x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₁ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₂ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₃ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₄ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₅ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₆ : (x ∈ s → edist (f x) b < ε ∧ f x ∈ t) → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mpr₁ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₂ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₃ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₄ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₅ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₆ : (edist x a < δ → f x ∈ t ∧ edist (f x) b < ε) → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mp₇ : ¬edist x a < δ → x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
mp₈ : x ∈ s → edist x a < δ → x ∉ s → f x ∈ t ∧ edist (f x) b < ε
mp₉ mp₁₀ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t ∧ edist (f x) b < ε
mp₁₁ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → f x ∈ t
mp₁₂ : x ∈ s → edist x a < δ → edist (f x) b < ε → f x ∈ t → edist (f x) b < ε
mpr₇ : x ∉ s → edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t
mpr₈ : edist x a < δ → x ∈ s → ¬edist x a < δ → edist (f x) b < ε ∧ f x ∈ t
mpr₉ mpr₁₀ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε ∧ f x ∈ t
mpr₁₁ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → edist (f x) b < ε
mpr₁₂ : edist x a < δ → x ∈ s → f x ∈ t → edist (f x) b < ε → f x ∈ t
⊢ edist x a < δ → x ∈ s → edist (f x) b < ε ∧ f x ∈ t ↔ x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε

Tactic:
tauto
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
b : β
rw :
  (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → Membership.mem (γ := Set β) univ (f x) ∧ edist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]

Premises used: nhdsWithin_univ, EMetric.tendsto_nhdsWithin_nhdsWithin
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
s : Set α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → Membership.mem (γ := Set β) univ (f x) ∧ edist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
simp only [mem_univ, true_and]

Premises used: Set.mem_univ, true_and
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε

Tactic:
nhds_basis_eball.tendsto_iff nhds_basis_eball

Premises used: Filter.HasBasis.tendsto_iff, Set.Mem, setOf, Metric.eball, Metric.nhds_basis_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
rw : Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
rw₁ rw₂ :
  (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) (f a) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds_nhds]

Premises used: ContinuousAt, EMetric.tendsto_nhds_nhds
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
a : α
s : Set α
rw : Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
rw₁ rw₂ :
  (∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → edist (f x) (f a) < ε

Tactic:
rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]

Premises used: ContinuousWithinAt, EMetric.tendsto_nhdsWithin_nhds
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, edist a b < δ → edist (f a) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff]

Premises used: EMetric.continuousWithinAt_iff, ContinuousOn
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      f ↔
    ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), edist a b < δ → edist (f a) (f b) < ε

Tactic:
continuous_iff_continuousAt.trans <| forall_congr' fun _ ↦ tendsto_nhds_nhds

Premises used: EMetric.tendsto_nhds_nhds, forall_congr', Iff.trans, continuous_iff_continuousAt
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
rw₁ rw₂ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, edist (f x) (f b) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds]

Premises used: ContinuousAt, EMetric.tendsto_nhds
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
rw₁ rw₂ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
rw [ContinuousWithinAt, tendsto_nhds]

Premises used: ContinuousWithinAt, EMetric.tendsto_nhds
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
simp [ContinuousOn, continuousWithinAt_iff']

Premises used: EMetric.continuousWithinAt_iff', ContinuousOn
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_1, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f ↔
    ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 a, edist (f x) (f a) < ε

Tactic:
continuous_iff_continuousAt.trans <| forall_congr' fun _ ↦ tendsto_nhds

Premises used: EMetric.tendsto_nhds, forall_congr', Iff.trans, continuous_iff_continuousAt
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (eball x ε)

Tactic:
EMetric.isOpen_iff.2 fun _ => exists_eball_subset_eball

Premises used: Iff.mpr, EMetric.isOpen_iff, Metric.exists_eball_subset_eball
-- Module: Mathlib.Topology.EMetricSpace.Defs
Goal:
α : Type u
inst : PseudoEMetricSpace α
x : α
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (eball x ∞)

Tactic:
isOpen_compl_iff.1 <| EMetric.isOpen_iff.2 fun _y hy =>
    ⟨⊤, ENNReal.coe_lt_top, fun _z hzy hzx =>
      hy (edistLtTopSetoid.trans (edistLtTopSetoid.symm hzy) hzx)⟩

Premises used: Iff.mpr, EMetric.isOpen_iff, Setoid.symm, And.intro, Exists.intro, Iff.mp, Setoid.trans, Top.top, isOpen_compl_iff, ENNReal.coe_lt_top