awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ Tendsto s atTop (𝓝 t)
have I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
Tactic: have I2 : ∀ n, ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n := by
    /- For the (much easier) reverse inequality, we start from a point `x ∈ t0` and we want
            to find a point `y ∈ s n` which is close to `x`.
            `x` belongs to `t0`, the intersection of the closures. In particular, it is well
            approximated by a point `z` in `⋃m≥n, s m`, say in `s m`. Since `s m` and
            `s n` are close, this point is itself well approximated by a point `y` in `s n`,
            as required. -/
    intro n x xt0
    have : x ∈ closure (⋃ m ≥ n, s m : Set α) := by apply mem_iInter.1 xt0 n
    obtain ⟨z : α, hz, Dxz : edist x z < B n⟩ := EMetric.mem_closure_iff.1 this (B n) (B_pos n)
    simp only [exists_prop, Set.mem_iUnion] at hz
    obtain ⟨m : ℕ, m_ge_n : m ≥ n, hm : z ∈ (s m : Set α)⟩ := hz
    have : hausdorffEDist (s m : Set α) (s n) < B n := hs n m n m_ge_n (le_refl n)
    obtain ⟨y : α, hy : y ∈ (s n : Set α), Dzy : edist z y < B n⟩ :=
      exists_edist_lt_of_hausdorffEDist_lt hm this
    exact
      ⟨y, hy,
        calc
          edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
          _ ≤ B n + B n := by gcongr
          _ = 2 * B n := (two_mul _).symm
          ⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ Tendsto s atTop (𝓝 t)
have main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
Tactic: have main : ∀ n : ℕ, edist (s n) t ≤ 2 * B n := fun n =>
    hausdorffEDist_le_of_mem_edist (I1 n) (I2 n)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
⊢ Tendsto s atTop (𝓝 t)
have h : ∀ (ε : ℝ≥0∞) (εpos : ε > 0), ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε
Tactic: refine EMetric.tendsto_atTop.2 fun ε εpos => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε
have this : 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)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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))
⊢ ∃ (N : ℕ), ∀ n ≥ N, edist (s n) t < ε
have this₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ 2 * B n) atTop (𝓝 0)
Tactic: rw [mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 : ℕ), ∀ n ≥ N, edist (s n) t < ε
have h : ∀ (N : ℕ) (hN : ∀ b ≥ N, ε > 2 * B b), ∃ (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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
s t : Compacts α
h : edist s t = 0
⊢ (↑s : Set α) = (↑t : Set α)
have this : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
⊢ (↑s : Set α) = (↑t : Set α)
have rwa : ∀ (this : (↑s : Set α) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)),
  (↑s : Set α) = (↑t : Set α)
Tactic: rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
⊢ (↑s : Set α) = (↑t : Set α)
have rwa₁ : ∀ (this : (↑s : Set α) = (↑t : Set α)), (↑s : Set α) = (↑t : Set α)
Tactic: rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
s t : NonemptyCompacts α
h : edist s t = 0
⊢ (↑s : Set α) = (↑t : Set α)
have this : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
⊢ (↑s : Set α) = (↑t : Set α)
have rwa : ∀ (this : (↑s : Set α) = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (↑t : Set α)),
  (↑s : Set α) = (↑t : Set α)
Tactic: rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
⊢ (↑s : Set α) = (↑t : Set α)
have rwa₁ : ∀ (this : (↑s : Set α) = (↑t : Set α)), (↑s : Set α) = (↑t : Set α)
Tactic: rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s : Set α
inst_2 : SecondCountableTopology α
⊢ SeparableSpace.{u_1} (NonemptyCompacts α)
have rcases : ∀ (s : Set α) (cs : s.Countable) (s_dense : Dense s), SeparableSpace.{u_1} (NonemptyCompacts α)
Tactic: rcases exists_countable_dense α with ⟨s, cs, s_dense⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
have refine_1 : v.Countable
Tactic: refine ⟨⟨v, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
⊢ SeparableSpace.{u_1} (NonemptyCompacts α)
have refine_2 : Dense v
Tactic: refine ⟨⟨v, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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}
⊢ v.Countable
have this : v0.Countable
Tactic: have : v0.Countable := countable_setOf_finite_subset cs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
have refine_2 : ∀ (t : NonemptyCompacts α) (ε : ℝ≥0∞) (εpos : ε > 0), ∃ y ∈ v, edist t y < ε
Tactic: refine fun t => EMetric.mem_closure_iff.2 fun ε εpos => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
⊢ ∃ y ∈ v, edist t y < ε
have refine_2 : ∀ (δ : ℝ≥0∞) (δpos : 0 < δ) (δlt : δ < ε), ∃ y ∈ v, edist t y < ε
Tactic: rcases exists_between εpos with ⟨δ, δpos, δlt⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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 : δ < ε
⊢ ∃ y ∈ v, edist t y < ε
have δpos' : 0 < δ / 2
Tactic: have δpos' : 0 < δ / 2 := ENNReal.half_pos δpos.ne'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
have rcases : ∀ (y : α) (ys : y ∈ s) (hy : 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⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ∃ y ∈ v, edist t y < ε
have Exy : ∀ (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⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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)
⊢ ∃ y ∈ v, edist t y < ε
have Fspec : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ∃ y ∈ v, edist t y < ε
have this : TotallyBounded (↑t : Set α)
Tactic: have : TotallyBounded (t : Set α) := t.isCompact.totallyBounded
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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 α)
⊢ ∃ y ∈ v, edist t y < ε
have refine_2 : ∀ (a : Set α) (af : a.Finite) (ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)), ∃ 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'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ∃ y ∈ v, edist t y < ε
have this₁ : b.Finite
Tactic: have : b.Finite := af.image _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
⊢ ∃ y ∈ b, edist x y < δ
have rcases : ∀ (z : α) (za : z ∈ a) (Dxz : x ∈ eball z (δ / 2)), ∃ y ∈ b, edist x y < δ
Tactic: rcases mem_iUnion₂.1 (ta hx) with ⟨z, za, Dxz⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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
z : α
za : z ∈ a
Dxz : x ∈ eball z (δ / 2)
⊢ ∃ y ∈ b, edist x y < δ
have exists : edist x (F z) < δ
Tactic: exists F z, mem_image_of_mem _ za
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
⊢ ∃ y ∈ v, edist t y < ε
have tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
Tactic: have tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ := by
        intro x hx
        rcases mem_iUnion₂.1 (ta hx) with ⟨z, za, Dxz⟩
        exists F z, mem_image_of_mem _ za
        calc
          edist x (F z) ≤ edist x z + edist z (F z) := edist_triangle _ _ _
          _ < δ / 2 + δ / 2 := ENNReal.add_lt_add Dxz (Fspec z).2
          _ = δ := ENNReal.add_halves _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
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
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
⊢ ∃ y ∈ v, edist t y < ε
have this₁ : c.Finite
Tactic: have : c.Finite := ‹b.Finite›.subset fun x hx => hx.1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
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_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this : c.Finite
x : α
hx : x ∈ t
⊢ ∃ y ∈ c, edist x y ≤ δ
have rcases : ∀ (y : α) (yv : y ∈ b) (Dxy : edist x y < δ), ∃ y ∈ c, edist x y ≤ δ
Tactic: rcases tb x hx with ⟨y, yv, Dxy⟩