awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
_ε : ℝ
ε0 : 0 < _ε
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < _ε
⊢ HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ) ≤ _ε

Tactic:
simpa using hn.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
r : ℝ
h0 : 0 < r
h1 : r < 1
⊢ (𝓤 α).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ {p : α × α | dist p.1 p.2 ≤ r ^ n}

Tactic:
Metric.mk_uniformity_basis_le (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
    let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
    ⟨n, trivial, hn.le⟩

Premises used: pow_pos, trivial, Exists, exists_pow_lt_of_lt_one, LT.lt.le, _private.0.Metric.uniformity_basis_dist_pow.match_1, LE.le, Metric.mk_uniformity_basis_le, And, HPow.hPow, And.intro, True, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s

Tactic:
uniformity_basis_dist.mem_uniformity_iff

Premises used: Filter.HasBasis.mem_uniformity_iff, Set.Mem, Metric.uniformity_basis_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
ε : ℝ
ε0 : 0 < ε
⊢ {p : α × α | dist p.1 p.2 < ε} ∈ 𝓤 α

Tactic:
mem_uniformity_dist.2 ⟨ε, ε0, fun _ _ ↦ id⟩

Premises used: Iff.mpr, id, Metric.mem_uniformity_dist, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
⊢ UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε

Tactic:
uniformity_basis_dist.uniformContinuous_iff uniformity_basis_dist

Premises used: Set.Mem, Metric.uniformity_basis_dist, Filter.HasBasis.uniformContinuous_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε

Tactic:
uniformity_basis_dist.uniformContinuousOn_iff uniformity_basis_dist

Premises used: Set.Mem, Metric.uniformity_basis_dist, Filter.HasBasis.uniformContinuousOn_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
⊢ UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b ≤ δ → dist (f a) (f b) ≤ ε

Tactic:
uniformity_basis_dist_le.uniformContinuous_iff uniformity_basis_dist_le

Premises used: Set.Mem, Metric.uniformity_basis_dist_le, Filter.HasBasis.uniformContinuous_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
⊢ UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist (f x) (f y) ≤ ε

Tactic:
uniformity_basis_dist_le.uniformContinuousOn_iff uniformity_basis_dist_le

Premises used: Set.Mem, Filter.HasBasis.uniformContinuousOn_iff, Metric.uniformity_basis_dist_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (x : ℝ) ↦ 0 < x) (ball x)

Tactic:
nhds_basis_uniformity uniformity_basis_dist

Premises used: Set.Mem, setOf, Metric.uniformity_basis_dist, Metric.ball, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ ε > 0, ball x ε ⊆ s

Tactic:
nhds_basis_ball.mem_iff

Premises used: Filter.HasBasis.mem_iff, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y

Tactic:
mem_nhds_iff

Premises used: Set.Mem, Filter.Eventually, setOf, Metric.ball, Set.Subset, Metric.mem_nhds_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
p : α → Prop
⊢ (∀ᶠ (y : α) in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ y ∈ ball x ε, p y

Tactic:
mem_nhds_iff

Premises used: Set.Mem, Filter.Eventually, setOf, Set.Subset, Metric.mem_nhds_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔
    ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Tactic:
(nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_

Premises used: Filter.basis_sets, Filter.HasBasis.eventually_iff, Iff.trans, Metric.nhds_basis_ball, Filter.HasBasis.prod
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
refine :
  (∃ (i : ℝ × Set ι), (0 < i.1 ∧ i.2 ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.1 ×ˢ id i.2 → p x) ↔
    ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)
⊢ (∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔
    ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Tactic:
refine (nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_

Premises used: Filter.basis_sets, Filter.HasBasis.eventually_iff, Iff.trans, Metric.nhds_basis_ball, Filter.HasBasis.prod
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∃ (i : ℝ × Set ι), (0 < i.1 ∧ i.2 ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.1 ×ˢ id i.2 → p x) ↔
    ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

Tactic:
simp only [Prod.exists, forall_prod_set, id, mem_ball, and_assoc, exists_and_left,
    Set.mem_surjective.exists, eventually_mem_set]

Premises used: Function.Surjective.exists, Set.forall_prod_set, exists_and_left, id, Set.mem_surjective, Metric.mem_ball, and_assoc, Prod.exists, Filter.eventually_mem_set
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
rw :
  (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
⊢ (∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]

Premises used: Filter.eventually_swap_iff, Metric.eventually_nhds_prod_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
mp :
  (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) →
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
mpr :
  (∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)) →
    ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap
⊢ (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ℝ
a2 : a1 > 0
a3 : ι → Prop
a4 : ∀ᶠ (i : ι) in f, a3 i
a5 : ∀ ⦃x : α⦄, dist x x₀ < a1 → ∀ ⦃i : ι⦄, a3 i → p (x, i).swap
⊢ ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ℝ
a2 : a1 > 0
a3 : ι → Prop
a4 : ∀ᶠ (i : ι) in f, a3 i
a5 : ∀ ⦃x : α⦄, dist x x₀ < a1 → ∀ ⦃i : ι⦄, a3 i → p (x, i).swap
⊢ ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ ⦃i : ι⦄, a1 i → ∀ ⦃x : α⦄, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Tactic:
⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ ⦃i : ι⦄, a1 i → ∀ ⦃x : α⦄, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Tactic:
exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) (closedBall x)

Tactic:
nhds_basis_uniformity uniformity_basis_dist_le

Premises used: Set.Mem, setOf, Metric.uniformity_basis_dist_le, Metric.closedBall, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ ball x (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
nhds_basis_uniformity uniformity_basis_dist_inv_nat_succ

Premises used: Set.Mem, setOf, Metric.uniformity_basis_dist_inv_nat_succ, Metric.ball, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (n : ℕ) ↦ 0 < n) fun (n : ℕ) ↦ ball x (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
nhds_basis_uniformity uniformity_basis_dist_inv_nat_pos

Premises used: Set.Mem, setOf, Metric.ball, nhds_basis_uniformity, Metric.uniformity_basis_dist_inv_nat_pos
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ closedBall x (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
nhds_basis_uniformity uniformity_basis_dist_le_inv_nat_succ

Premises used: Set.Mem, setOf, Metric.uniformity_basis_dist_le_inv_nat_succ, Metric.closedBall, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (n : ℕ) ↦ 0 < n) fun (n : ℕ) ↦ closedBall x (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
nhds_basis_uniformity uniformity_basis_dist_le_inv_nat_pos

Premises used: Metric.uniformity_basis_dist_le_inv_nat_pos, Set.Mem, setOf, Metric.closedBall, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
r : ℝ
h0 : 0 < r
h1 : r < 1
⊢ (𝓝 x).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ ball x (r ^ n)

Tactic:
nhds_basis_uniformity (uniformity_basis_dist_pow h0 h1)

Premises used: Set.Mem, setOf, Metric.ball, Metric.uniformity_basis_dist_pow, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
r : ℝ
h0 : 0 < r
h1 : r < 1
⊢ (𝓝 x).HasBasis (fun (x : ℕ) ↦ True) fun (n : ℕ) ↦ closedBall x (r ^ n)

Tactic:
nhds_basis_uniformity (uniformity_basis_dist_le_pow h0 h1)

Premises used: Set.Mem, setOf, Metric.closedBall, Metric.uniformity_basis_dist_le_pow, nhds_basis_uniformity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s

Tactic:
simp only [isOpen_iff_mem_nhds, mem_nhds_iff]

Premises used: Metric.mem_nhds_iff, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x ε)

Tactic:
isOpen_iff.2 fun _ => exists_ball_subset_ball

Premises used: Iff.mpr, Metric.isOpen_iff, Metric.exists_ball_subset_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
ε0 : 0 < ε
⊢ ball x ε ∈ 𝓝 x

Tactic:
isOpen_ball.mem_nhds (mem_ball_self ε0)

Premises used: Metric.mem_ball_self, Metric.isOpen_ball, IsOpen.mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
ε0 : 0 < ε
⊢ closedBall x ε ∈ 𝓝 x

Tactic:
mem_of_superset (ball_mem_nhds x ε0) ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Metric.ball_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x c : α
ε : ℝ
h : x ∈ ball c ε
⊢ closedBall c ε ∈ 𝓝 x

Tactic:
mem_of_superset (isOpen_ball.mem_nhds h) ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Metric.isOpen_ball, IsOpen.mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
s : Set α
⊢ (𝓝[s] x).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ ball x ε ∩ s

Tactic:
nhdsWithin_hasBasis nhds_basis_ball s

Premises used: nhdsWithin_hasBasis, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
s t : Set α
⊢ s ∈ 𝓝[t] x ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s

Tactic:
nhdsWithin_basis_ball.mem_iff

Premises used: Filter.HasBasis.mem_iff, Metric.nhdsWithin_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
s : Set α
inst_1 : PseudoMetricSpace β
t : Set β
f : α → β
a : α
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ (ia : ℝ), 0 < ia ∧ ∀ x ∈ ball a ia ∩ s, f x ∈ ball b ib ∩ t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε

Tactic:
simp only [inter_comm _ s, inter_comm _ t, mem_inter_iff, and_imp, gt_iff_lt, mem_ball]

Premises used: and_imp, Set.mem_inter_iff, Metric.mem_ball, Set.inter_comm, gt_iff_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
s : Set α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
b : β
rw :
  (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → Membership.mem (γ := Set β) univ (f x) ∧ dist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Tactic:
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]

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

Tactic:
simp only [mem_univ, true_and]

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

Tactic:
nhds_basis_ball.tendsto_iff nhds_basis_ball

Premises used: Filter.HasBasis.tendsto_iff, Set.Mem, Metric.ball, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
rw : Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
rw₁ rw₂ :
  (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds_nhds]

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

Tactic:
rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]

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

Tactic:
simp [ContinuousOn, continuousWithinAt_iff]

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

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

Premises used: Metric.tendsto_nhds_nhds, forall_congr', Iff.trans, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε

Tactic:
nhds_basis_ball.tendsto_right_iff

Premises used: Set.Mem, Metric.ball, Metric.nhds_basis_ball, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
rw₁ rw₂ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds]

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

Tactic:
rw [ContinuousWithinAt, tendsto_nhds]

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

Tactic:
simp [ContinuousOn, continuousWithinAt_iff']

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

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

Premises used: Metric.tendsto_nhds, forall_congr', Iff.trans, continuous_iff_continuousAt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
u : β → α
a : α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ici ia, u x ∈ ball a ib) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, dist (u n) a < ε

Tactic:
simp only [true_and, mem_ball, mem_Ici]

Premises used: Metric.mem_ball, Set.mem_Ici, true_and
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Nonempty β
inst_2 : SemilatticeSup β
inst_3 : NoMaxOrder β
u : β → α
a : α
⊢ (∀ (ib : ℝ), 0 < ib → ∃ (ia : β), True ∧ ∀ x ∈ Ioi ia, u x ∈ ball a ib) ↔
    ∀ ε > 0, ∃ (N : β), ∀ n > N, dist (u n) a < ε

Tactic:
simp only [true_and, gt_iff_lt, mem_Ioi, mem_ball]

Premises used: Set.mem_Ioi, Metric.mem_ball, gt_iff_lt, true_and
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
inst : PseudoMetricSpace α
x : α
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x

Tactic:
simp [isOpen_iff, subset_singleton_iff, mem_ball]

Premises used: Set.subset_singleton_iff, Metric.mem_ball, Metric.isOpen_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ (ball x ε).Nonempty

Tactic:
simp [hε]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ (ball x ε).Nonempty

Tactic:
have : (ball x ε).Nonempty := by simp [hε]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
this : (ball x ε).Nonempty
⊢ ∃ y ∈ s, dist x y < ε

Tactic:
simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

Premises used: Metric.isOpen_ball, Dense.exists_mem_open, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
f : β → α
hf : DenseRange f
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ (y : β), dist x (f y) < ε

Tactic:
exists_range_iff.1 (hf.exists_dist_lt x hε)

Premises used: Dense.exists_dist_lt, Set.exists_range_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ Eq.{u + 1} (α := UniformSpace α) PseudoMetricSpace.toUniformSpace ⊥ ↔
    ∃ (r : ℝ), 0 < r ∧ Pairwise fun (x1 x2 : α) ↦ r ≤ dist x1 x2

Tactic:
simp only [uniformity_basis_dist.uniformSpace_eq_bot, mem_setOf_eq, not_lt]

Premises used: Metric.uniformity_basis_dist, Set.mem_setOf_eq, not_lt, Filter.HasBasis.uniformSpace_eq_bot
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
inst : PseudoMetricSpace α
r : ℝ
hpos : 0 < r
hr : Pairwise fun (x1 x2 : α) ↦ r ≤ dist x1 x2
rw : Eq.{u_3 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace ⊥
rw₁ rw₂ : Eq.{u_3 + 1} (α := TopologicalSpace α) ⊥ ⊥
⊢ Eq.{u_3 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace ⊥

Tactic:
rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]

Premises used: Iff.mpr, UniformSpace.toTopologicalSpace_bot, And.intro, Exists.intro, Metric.uniformSpace_eq_bot