awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
⊢ Tendsto (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 (HMul.hMul (α := ℝ≥0∞) 2 0))

Tactic:
have : Tendsto (fun n => 2 * B n) atTop (𝓝 (2 * 0)) :=
    ENNReal.Tendsto.const_mul (ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one <|
      by simp) (Or.inr <| by simp)
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 (HMul.hMul (α := ℝ≥0∞) 2 0))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 0)

Tactic:
rw [mul_zero] at this

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 0)
⊢ ∃ (N : ℕ), ∀ b ≥ N, ε > 2 * B b

Tactic:
((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop

Premises used: tendsto_order, And.right, Iff.mp, Filter.Eventually.exists_forall_of_atTop
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 0)
h : ∀ (N : ℕ) (hN : ∀ b ≥ N, ε > 2 * B b), ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε

Tactic:
obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b :=
    ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop

Premises used: tendsto_order, And.right, Iff.mp, Filter.Eventually.exists_forall_of_atTop
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 0)
N : ℕ
hN : ∀ b ≥ N, ε > 2 * B b
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε

Tactic:
⟨N, fun n hn => lt_of_le_of_lt (main n) (hN n hn)⟩

Premises used: lt_of_le_of_lt, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ HPow.hPow (α := ℝ≥0∞) 2⁻¹ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α :=
  ⋂ (n : ℕ), closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ (m : ℕ), ⋃ (_ : m ≥ n), (↑(s m) : Set α))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 0)
N : ℕ
hN : ∀ b ≥ N, ε > 2 * B b
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε

Tactic:
exact ⟨N, fun n hn => lt_of_le_of_lt (main n) (hN n hn)⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Isometry (β := Closeds α) fun (x : α) ↦ {x}

Tactic:
fun _ _ => hausdorffEDist_singleton

Premises used: setOf, Set.singleton, Metric.hausdorffEDist_singleton, Isometry
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ LipschitzWith (β := Closeds α) 1 fun (p : Closeds α × Closeds α) ↦ p.1 ⊔ p.2

Tactic:
.of_edist_le fun _ _ => hausdorffEDist_union_le

Premises used: LipschitzWith.of_edist_le, Metric.hausdorffEDist_union_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
⊢ LipschitzWith (β := Closeds (α × β)) 1 fun (p : Prod.{u_1, u_2} (Closeds α) (Closeds β)) ↦ p.1 ×ˢ p.2

Tactic:
.of_edist_le fun _ _ => hausdorffEDist_prod_le

Premises used: LipschitzWith.of_edist_le, Metric.hausdorffEDist_prod_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
⊢ Eq.{u_1 + 1} (α := Filter (Compacts α × Compacts α)) (uniformity (Compacts α)) (uniformity (Compacts α))

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
s t : Compacts α
h : edist s t = 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α) =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)

Tactic:
have : closure (s : Set α) = closure t := hausdorffEDist_zero_iff_closure_eq_closure.1 h
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
s t : Compacts α
h : edist s t = 0
this :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α) =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)
rwa :
  ∀ (this : (↑s : Set α) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)),
    (↑s : Set α) = (↑t : Set α)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (↑s : Set α) = (↑t : Set α)), (↑s : Set α) = (↑t : Set α)
⊢ (↑s : Set α) = (↑t : Set α)

Tactic:
rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

Premises used: IsClosed.closure_eq, TopologicalSpace.Compacts.isCompact, IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
s t : Compacts α
⊢ edist s t = hausdorffEDist (↑s : Set α) (↑t : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Isometry.{u_1, u_1} (α := Compacts α) toCloseds

Tactic:
fun _ _ => rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Isometry (β := Compacts α) fun (x : α) ↦ {x}

Tactic:
fun _ _ => hausdorffEDist_singleton

Premises used: setOf, Set.singleton, Metric.hausdorffEDist_singleton, Isometry
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ LipschitzWith (β := Compacts α) 1 fun (p : Compacts α × Compacts α) ↦ p.1 ⊔ p.2

Tactic:
.of_edist_le fun _ _ => hausdorffEDist_union_le

Premises used: LipschitzWith.of_edist_le, Metric.hausdorffEDist_union_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
⊢ LipschitzWith (β := Compacts (α × β)) 1 fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦ p.1 ×ˢ p.2

Tactic:
.of_edist_le fun _ _ => hausdorffEDist_prod_le

Premises used: LipschitzWith.of_edist_le, Metric.hausdorffEDist_prod_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
⊢ Eq.{u_1 + 1} (α := Filter (NonemptyCompacts α × NonemptyCompacts α)) (uniformity (NonemptyCompacts α))
    (uniformity (NonemptyCompacts α))

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
s t : NonemptyCompacts α
h : edist s t = 0
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α) =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)

Tactic:
have : closure (s : Set α) = closure t := hausdorffEDist_zero_iff_closure_eq_closure.1 h
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
s t : NonemptyCompacts α
h : edist s t = 0
this :
  closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set α) =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)
rwa :
  ∀ (this : (↑s : Set α) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)),
    (↑s : Set α) = (↑t : Set α)
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : (↑s : Set α) = (↑t : Set α)), (↑s : Set α) = (↑t : Set α)
⊢ (↑s : Set α) = (↑t : Set α)

Tactic:
rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this

Premises used: IsClosed.closure_eq, TopologicalSpace.NonemptyCompacts.isCompact, IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Isometry.{u_1, u_1} (α := NonemptyCompacts α) toCloseds

Tactic:
fun _ _ => rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Isometry.{u_1, u_1} (α := NonemptyCompacts α) toCompacts

Tactic:
fun _ _ => rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
inst_1 : CompleteSpace α
⊢ IsClosed.{u_1} (X := Closeds α) (range toCloseds)

Tactic:
NonemptyCompacts.isClosedEmbedding_toCloseds.isClosed_range

Premises used: TopologicalSpace.NonemptyCompacts.isClosedEmbedding_toCloseds, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : SecondCountableTopology α
rcases : ∀ (s : Set α) (cs : s.Countable) (s_dense : Dense s), SeparableSpace.{u_1} (NonemptyCompacts α)
⊢ SeparableSpace.{u_1} (NonemptyCompacts α)

Tactic:
rcases exists_countable_dense α with ⟨s, cs, s_dense⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
⊢ SeparableSpace.{u_1} (NonemptyCompacts α)

Tactic:
⟨⟨v, ?_, ?_⟩⟩

Premises used: And.intro, Exists.intro, TopologicalSpace.SeparableSpace.mk
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
refine_1 : v.Countable
refine_2 : Dense v
⊢ SeparableSpace.{u_1} (NonemptyCompacts α)

Tactic:
refine ⟨⟨v, ?_, ?_⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
⊢ v0.Countable

Tactic:
have : v0.Countable := countable_setOf_finite_subset cs
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
this : v0.Countable
⊢ v.Countable

Tactic:
this.preimage SetLike.coe_injective

Premises used: SetLike.coe_injective, Set.preimage, Set.Countable.preimage
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
this : v0.Countable
⊢ v.Countable

Tactic:
exact this.preimage SetLike.coe_injective

Premises used: SetLike.coe_injective, Set.Countable.preimage
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
⊢ Dense v

Tactic:
fun t => EMetric.mem_closure_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Set.Mem, Dense, EMetric.mem_closure_iff
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
refine_2 : ∀ (t : NonemptyCompacts α) (ε : ℝ≥0∞) (εpos : ε > 0), ∃ y ∈ v, edist t y < ε
⊢ Dense v

Tactic:
refine fun t => EMetric.mem_closure_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, EMetric.mem_closure_iff
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
refine_2 : ∀ (δ : ℝ≥0∞) (δpos : 0 < δ) (δlt : δ < ε), ∃ y ∈ v, edist t y < ε
⊢ ∃ y ∈ v, edist t y < ε

Tactic:
rcases exists_between εpos with ⟨δ, δpos, δlt⟩

Premises used: exists_between
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
⊢ 0 < δ / 2

Tactic:
have δpos' : 0 < δ / 2 := ENNReal.half_pos δpos.ne'
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
x : α
rcases : ∀ (y : α) (ys : y ∈ s) (hy : edist x y < δ / 2), ∃ y ∈ s, edist x y < δ / 2
⊢ ∃ y ∈ s, edist x y < δ / 2

Tactic:
rcases EMetric.mem_closure_iff.1 (s_dense x) (δ / 2) δpos' with ⟨y, ys, hy⟩

Premises used: HDiv.hDiv, Iff.mp, EMetric.mem_closure_iff, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
x y : α
ys : y ∈ s
hy : edist x y < δ / 2
⊢ ∃ y ∈ s, edist x y < δ / 2

Tactic:
⟨y, ⟨ys, hy⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
x y : α
ys : y ∈ s
hy : edist x y < δ / 2
⊢ ∃ y ∈ s, edist x y < δ / 2

Tactic:
exact ⟨y, ⟨ys, hy⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
⊢ ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2

Tactic:
have Exy : ∀ x, ∃ y, y ∈ s ∧ edist x y < δ / 2 := by
        intro x
        rcases EMetric.mem_closure_iff.1 (s_dense x) (δ / 2) δpos' with ⟨y, ys, hy⟩
        exact ⟨y, ⟨ys, hy⟩⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
⊢ ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2

Tactic:
have Fspec : ∀ x, F x ∈ s ∧ edist x (F x) < δ / 2 := fun x => (Exy x).choose_spec
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
⊢ TotallyBounded (↑t : Set α)

Tactic:
have : TotallyBounded (t : Set α) := t.isCompact.totallyBounded
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this : TotallyBounded (↑t : Set α)
refine_2 : ∀ (a : Set α) (af : a.Finite) (ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)), ∃ y ∈ v, edist t y < ε
⊢ ∃ y ∈ v, edist t y < ε

Tactic:
obtain ⟨a : Set α, af : Set.Finite a, ta : (t : Set α) ⊆ ⋃ y ∈ a, Metric.eball y (δ / 2)⟩ :=
        EMetric.totallyBounded_iff.1 this (δ / 2) δpos'

Premises used: HDiv.hDiv, SetLike.coe, EMetric.totallyBounded_iff, Iff.mp, OfNat.ofNat, Set
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
⊢ b.Finite

Tactic:
have : b.Finite := af.image _
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this : b.Finite
x : α
hx : x ∈ t
rcases : ∀ (z : α) (za : z ∈ a) (Dxz : x ∈ eball z (δ / 2)), ∃ y ∈ b, edist x y < δ
⊢ ∃ y ∈ b, edist x y < δ

Tactic:
rcases mem_iUnion₂.1 (ta hx) with ⟨z, za, Dxz⟩

Premises used: Set.mem_iUnion₂, Iff.mp