awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε ⊆ interior (closedBall x ε)

Tactic:
interior_maximal ball_subset_closedBall isOpen_ball

Premises used: Metric.ball_subset_closedBall, interior_maximal, Metric.isOpen_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
a : α
⊢ (∀ (i : ℝ), 0 < i → ∃ y ∈ s, y ∈ ball a i) ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
simp only [mem_ball, dist_comm]

Premises used: dist_comm, Metric.mem_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
e : β → α
a : α
⊢ a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range e) ↔ ∀ ε > 0, ∃ (k : β), dist a (e k) < ε

Tactic:
simp only [mem_closure_iff, exists_range_iff]

Premises used: Metric.mem_closure_iff, Set.exists_range_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
e : β → α
a : α
⊢ (∀ (i : ℕ), True → ∃ y ∈ range e, y ∈ ball a (1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1)) ↔
    ∀ (n : ℕ), ∃ (k : β), dist a (e k) < 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp only [mem_ball, dist_comm, exists_range_iff, forall_const]

Premises used: dist_comm, Metric.mem_ball, Set.exists_range_iff, forall_const
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
a : α
⊢ a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a

Premises used: IsClosed.closure_eq, Metric.mem_closure_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ↔ ∀ r > 0, (ball x r ∩ s).Nonempty

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

Premises used: Set.mem_inter_iff, Metric.mem_closure_iff, and_comm, Set.Nonempty, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
simp_rw₁ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ (i : α) (_ : i ∈ s), x ∈ ball i r
simp_rw₂ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, x ∈ ball i r
simp_rw₃ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
simp_rw₄ :
  (∀ (x : α), x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ↔
    ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
simp_rw₅ : (∀ (x : α), ∀ ε > 0, ∃ b ∈ s, dist x b < ε) ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ

Tactic:
simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion, forall_comm, Dense, Metric.mem_closure_iff, exists_prop, Metric.mem_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
x : α
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (range f) ↔ ∀ r > 0, ∃ (y : β), dist x (f y) < r

Tactic:
simp only [mem_closure_iff, exists_range_iff]

Premises used: Metric.mem_closure_iff, Set.exists_range_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : X
⊢ nndist (α := Additive X) ((ofMul : (a : X) → Additive X) a : Additive X)
      ((ofMul : (a : X) → Additive X) b : Additive X) =
    nndist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : X
⊢ nndist (α := Multiplicative X) ((ofAdd : (a : X) → Multiplicative X) a : Multiplicative X)
      ((ofAdd : (a : X) → Multiplicative X) b : Multiplicative X) =
    nndist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : Additive X
⊢ nndist (α := X) ((toMul : (a : Additive X) → X) a : X) ((toMul : (a : Additive X) → X) b : X) = nndist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : Multiplicative X
⊢ nndist (α := X) ((toAdd : (a : Multiplicative X) → X) a : X) ((toAdd : (a : Multiplicative X) → X) b : X) = nndist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : X
⊢ nndist (α := Xᵒᵈ) ((toDual : (a : X) → Xᵒᵈ) a : Xᵒᵈ) ((toDual : (a : X) → Xᵒᵈ) b : Xᵒᵈ) = nndist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
X : Type u_1
inst : PseudoMetricSpace X
a b : Xᵒᵈ
⊢ nndist (α := X) ((ofDual : (a : Xᵒᵈ) → X) a : X) ((ofDual : (a : Xᵒᵈ) → X) b : X) = nndist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
ι : Type u_1
α : Type u_2
inst : PseudoMetricSpace α
x : ℝ
⊢ 𝓝 x = ⨅ (r : ℝ), ⨅ (_ : r > 0), 𝓟 {b : ℝ | |x - b| < r}

Tactic:
simp only [nhds_basis_ball.eq_biInf, ball, Real.dist_eq, abs_sub_comm]

Premises used: Metric.ball, Filter.HasBasis.eq_biInf, Real.dist_eq, abs_sub_comm, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
b : ℝ
⊢ Eq (α := Set ℝ) {b} (⋂ (r : ℝ), ⋂ (_ : r > 0), Icc (b - r) (b + r))

Tactic:
simp [Icc_eq_closedBall, biInter_basis_nhds Metric.nhds_basis_closedBall]

Premises used: biInter_basis_nhds, Metric.nhds_basis_closedBall, Real.Icc_eq_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_3
f g : α → ℝ
t₀ : Filter α
hf : ∀ᶠ (t : α) in t₀, 0 ≤ f t
hft : ∀ᶠ (t : α) in t₀, f t ≤ g t
g0 : Tendsto g t₀ (𝓝 0)
⊢ Tendsto f t₀ (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds g0 hf hft

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_3
f g : α → ℝ
t₀ : Filter α
hf : ∀ (t : α), 0 ≤ f t
hft : ∀ (t : α), f t ≤ g t
g0 : Tendsto g t₀ (𝓝 0)
⊢ Tendsto f t₀ (𝓝 0)

Tactic:
squeeze_zero' (Eventually.of_forall hf) (Eventually.of_forall hft) g0

Premises used: Filter.Eventually.of_forall, squeeze_zero'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
⊢ ∃ (ε : ℝ), 0 < ε ∧ closedBall x ε ⊆ u

Tactic:
nhds_basis_closedBall.mem_iff.1 hu

Premises used: Filter.HasBasis.mem_iff, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : closedBall x ε ⊆ u), ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu

Premises used: Filter.HasBasis.mem_iff, Iff.mp, Metric.nhds_basis_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ Membership.mem (γ := Filter ℝ) (𝓝 0) (Iic ε)

Tactic:
have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Membership.mem (γ := Filter ℝ) (𝓝 0) (Iic ε)
a : ℝ
hr : a ∈ Iic ε
⊢ closedBall x a ⊆ u

Tactic:
Subset.trans (closedBall_subset_closedBall hr) hε

Premises used: Set.Subset.trans, Metric.closedBall_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Membership.mem (γ := Filter ℝ) (𝓝 0) (Iic ε)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ | x_1 ∈ Iic ε → Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (r : ℝ) ↦ closedBall x r ⊆ u) x_2} x_1} a
h₁ h₂ : ∀ (a : ℝ) (hr : a ∈ Iic ε), closedBall x a ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
⊢ Tendsto (closedBall x) (𝓝 0) (𝓝 x).smallSets

Tactic:
tendsto_smallSets_iff.2 fun _ ↦ eventually_closedBall_subset

Premises used: Iff.mpr, Filter.tendsto_smallSets_iff, eventually_closedBall_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, ball x r ⊆ u

Tactic:
(eventually_closedBall_subset hu).mono fun _r hr ↦ ball_subset_closedBall.trans hr

Premises used: Metric.ball_subset_closedBall, HasSubset.Subset.trans, Filter.Eventually.mono, eventually_closedBall_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (y : α) ↦ dist y x

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (closedBall x ε) = closedBall x ε

Tactic:
isClosed_closedBall.closure_eq

Premises used: Metric.isClosed_closedBall, IsClosed.closure_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (sphere x ε) = sphere x ε

Tactic:
isClosed_sphere.closure_eq

Premises used: IsClosed.closure_eq, Metric.isClosed_sphere
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball x ε) ⊆ closedBall x ε

Tactic:
closure_minimal ball_subset_closedBall isClosed_closedBall

Premises used: Metric.ball_subset_closedBall, closure_minimal, Metric.isClosed_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
⊢ closedBall x 0 = closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x}

Tactic:
Subset.antisymm
    (fun _y hy =>
      mem_closure_iff.2 fun _ε ε0 => ⟨x, mem_singleton x, (mem_closedBall.1 hy).trans_lt ε0⟩)
    (closure_minimal (singleton_subset_iff.2 (dist_self x).le) isClosed_closedBall)

Premises used: Set.Subset.antisymm, Iff.mpr, Set.mem_singleton, Set.singleton_subset_iff, closure_minimal, Metric.isClosed_closedBall, Eq.le, Metric.mem_closure_iff, dist_self, And.intro, Exists.intro, Iff.mp, Metric.mem_closedBall, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
rcases : ∀ (s : Set α) (s_compact : IsCompact s) (hs : s ∈ 𝓝 x), ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Tactic:
rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
h : ∀ (r : ℝ) (hr : closedBall x r ⊆ s), IsCompact (closedBall x r)
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)

Tactic:
filter_upwards [eventually_closedBall_subset hs] with r hr

Premises used: eventually_closedBall_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
r : ℝ
hr : closedBall x r ⊆ s
⊢ IsCompact (closedBall x r)

Tactic:
IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

Premises used: Metric.isClosed_closedBall, IsCompact.of_isClosed_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
r : ℝ
hr : closedBall x r ⊆ s
⊢ IsCompact (closedBall x r)

Tactic:
exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

Premises used: Metric.isClosed_closedBall, IsCompact.of_isClosed_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, IsCompact (closedBall x r)

Tactic:
have : ∀ᶠ r in 𝓝[>] 0, IsCompact (closedBall x r) :=
    eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
this : ∀ᶠ (r : ℝ) in 𝓝[>] 0, IsCompact (closedBall x r)
⊢ ∃ (r : ℝ), 0 < r ∧ IsCompact (closedBall x r)

Tactic:
simpa only [and_comm] using (this.and self_mem_nhdsWithin).exists

Premises used: Filter.Eventually.and, and_comm, Filter.Eventually.exists, self_mem_nhdsWithin
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋂ (r' : ℝ), ⋂ (_ : r' > r), closedBall x r') x_1 ↔ x_1 ∈ closedBall x r
⊢ ⋂ (r' : ℝ), ⋂ (_ : r' > r), closedBall x r' = closedBall x r

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
⊢ Membership.mem (γ := Set α) (⋂ (r' : ℝ), ⋂ (_ : r' > r), closedBall x r') x_1 ↔ x_1 ∈ closedBall x r

Tactic:
simp [forall_gt_imp_ge_iff_le_of_dense]

Premises used: forall_gt_imp_ge_iff_le_of_dense
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋂ (r' : ℝ), ⋂ (_ : r' > r), ball x r') x_1 ↔ x_1 ∈ closedBall x r
⊢ ⋂ (r' : ℝ), ⋂ (_ : r' > r), ball x r' = closedBall x r

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
⊢ Membership.mem (γ := Set α) (⋂ (r' : ℝ), ⋂ (_ : r' > r), ball x r') x_1 ↔ x_1 ∈ closedBall x r

Tactic:
simp [forall_gt_iff_le]

Premises used: forall_gt_iff_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r') x_1 ↔ x_1 ∈ ball x r
⊢ ⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r' = ball x r

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
h : x_1 ∉ ⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r' ↔ x_1 ∉ ball x r
⊢ Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r') x_1 ↔ x_1 ∈ ball x r

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
⊢ x_1 ∉ ⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r' ↔ x_1 ∉ ball x r

Tactic:
simp [forall_lt_imp_le_iff_le_of_dense]

Premises used: forall_lt_imp_le_iff_le_of_dense
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r') x_1 ↔ x_1 ∈ ball x r
⊢ ⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r' = ball x r

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
h : x_1 ∉ ⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r' ↔ x_1 ∉ ball x r
⊢ Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r') x_1 ↔ x_1 ∈ ball x r

Tactic:
rw [← not_iff_not]

Premises used: not_iff_not
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
⊢ x_1 ∉ ⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r' ↔ x_1 ∉ ball x r

Tactic:
simp [forall_lt_iff_le]

Premises used: forall_lt_iff_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ι : Sort u_3
c : ι → Set α
hs : IsCompact s
hc₁ : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (c i)
hc₂ : s ⊆ ⋃ (i : ι), c i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ (i : ι), ball x δ ⊆ c i

Tactic:
simpa only [ball, UniformSpace.ball, preimage_setOf_eq, dist_comm]
    using uniformity_basis_dist.lebesgue_number_lemma hs hc₁ hc₂

Premises used: Metric.uniformity_basis_dist, Metric.ball, dist_comm, UniformSpace.ball, Set.preimage_setOf_eq, Filter.HasBasis.lebesgue_number_lemma
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃₀ c
⊢ s ⊆ ⋃ (i : (↑c : Type u_2)), (↑i : Set α)

Tactic:
rw [sUnion_eq_iUnion] at hc₂

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ (i : (↑c : Type u_2)), (↑i : Set α)
⊢ ∀ (i : (↑c : Type u_2)), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑i : Set α)

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ (i : (↑c : Type u_2)), (↑i : Set α)
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Tactic:
simpa using lebesgue_number_lemma_of_metric hs (by simpa) hc₂

Premises used: lebesgue_number_lemma_of_metric
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
⊢ edist f g =
    ENNReal.ofReal ((fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) f g)

Tactic:
simp [edist_pi_def]

Premises used: edist_pi_def
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
refine : ∀ (s : Set ((b : β) → X b)), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ PseudoMetricSpace ((b : β) → X b)

Tactic:
refine i.replaceBornology fun s => ?_

Premises used: PseudoMetricSpace.replaceBornology
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
simp :
  (∀ᶠ (x : ℝ) in atTop,
      ∀ (i : β) ⦃x_1 : (x : β) → X x⦄,
        x_1 ∈ s →
          ∀ ⦃x_2 : (x : β) → X x⦄,
            x_2 ∈ s → (↑(nndist (Function.eval (β := X) i x_1) (Function.eval (β := X) i x_2)) : ℝ) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
simp only [isBounded_iff_eventually, ← forall_isBounded_image_eval_iff,
    forall_mem_image, ← Filter.eventually_all, @dist_nndist (X _)]

Premises used: Metric.isBounded_iff_eventually, Filter.eventually_all, dist_nndist, Bornology.forall_isBounded_image_eval_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
⊢ (∀ᶠ (x : ℝ) in atTop,
      ∀ (i : β) ⦃x_1 : (x : β) → X x⦄,
        x_1 ∈ s →
          ∀ ⦃x_2 : (x : β) → X x⦄,
            x_2 ∈ s → (↑(nndist (Function.eval (β := X) i x_1) (Function.eval (β := X) i x_2)) : ℝ) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C

Tactic:
eventually_congr ((eventually_ge_atTop 0).mono fun C hC ↦ ?_)

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop, Filter.eventually_congr, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
refine :
  ∀ (C : ℝ) (hC : 0 ≤ C),
    (∀ (i : β) ⦃x : (x : β) → X x⦄,
        x ∈ s →
          ∀ ⦃x_1 : (x : β) → X x⦄,
            x_1 ∈ s → (↑(nndist (Function.eval (β := X) i x) (Function.eval (β := X) i x_1)) : ℝ) ≤ C) ↔
      ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C
⊢ (∀ᶠ (x : ℝ) in atTop,
      ∀ (i : β) ⦃x_1 : (x : β) → X x⦄,
        x_1 ∈ s →
          ∀ ⦃x_2 : (x : β) → X x⦄,
            x_2 ∈ s → (↑(nndist (Function.eval (β := X) i x_1) (Function.eval (β := X) i x_2)) : ℝ) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C

Tactic:
refine eventually_congr ((eventually_ge_atTop 0).mono fun C hC ↦ ?_)

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop, Filter.eventually_congr, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ
hC : 0 ≤ C
⊢ 0 ≤ C

Tactic:
hC
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ
hC : 0 ≤ C
lift :
  ∀ (C : ℝ≥0),
    (∀ (i : β) ⦃x : (x : β) → X x⦄,
        x ∈ s →
          ∀ ⦃x_1 : (x : β) → X x⦄,
            x_1 ∈ s → (↑(nndist (Function.eval (β := X) i x) (Function.eval (β := X) i x_1)) : ℝ) ≤ (↑C : ℝ)) ↔
      ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ (↑C : ℝ)
⊢ (∀ (i : β) ⦃x : (x : β) → X x⦄,
      x ∈ s →
        ∀ ⦃x_1 : (x : β) → X x⦄,
          x_1 ∈ s → (↑(nndist (Function.eval (β := X) i x) (Function.eval (β := X) i x_1)) : ℝ) ≤ C) ↔
    ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C

Tactic:
lift C to ℝ≥0 using hC