[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ Continuous fun p => infEdist p.fst ↑p.snd
[PROOFSTEP]
refine' continuous_of_le_add_edist 2 (by simp) _
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ 2 ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
⊢ ∀ (x y : α × Closeds α), infEdist x.fst ↑x.snd ≤ infEdist y.fst ↑y.snd + 2 * edist x y
[PROOFSTEP]
rintro ⟨x, s⟩ ⟨y, t⟩
[GOAL]
case mk.mk
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist (x, s).fst ↑(x, s).snd ≤ infEdist (y, t).fst ↑(y, t).snd + 2 * edist (x, s) (y, t)
[PROOFSTEP]
calc
  infEdist x s ≤ infEdist x t + hausdorffEdist (t : Set α) s := infEdist_le_infEdist_add_hausdorffEdist
  _ ≤ infEdist y t + edist x y + hausdorffEdist (t : Set α) s := (add_le_add_right infEdist_le_infEdist_add_edist _)
  _ = infEdist y t + (edist x y + hausdorffEdist (s : Set α) t) := by rw [add_assoc, hausdorffEdist_comm]
  _ ≤ infEdist y t + (edist (x, s) (y, t) + edist (x, s) (y, t)) :=
    (add_le_add_left (add_le_add (le_max_left _ _) (le_max_right _ _)) _)
  _ = infEdist y t + 2 * edist (x, s) (y, t) := by rw [← mul_two, mul_comm]
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist y ↑t + edist x y + hausdorffEdist ↑t ↑s = infEdist y ↑t + (edist x y + hausdorffEdist ↑s ↑t)
[PROOFSTEP]
rw [add_assoc, hausdorffEdist_comm]
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEdist y ↑t + (edist (x, s) (y, t) + edist (x, s) (y, t)) = infEdist y ↑t + 2 * edist (x, s) (y, t)
[PROOFSTEP]
rw [← mul_two, mul_comm]
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
⊢ IsClosed {t | ↑t ⊆ s}
[PROOFSTEP]
refine'
  isClosed_of_closure_subset fun t ht x hx =>
    _
      -- t : Closeds α, ht : t ∈ closure {t : Closeds α | t ⊆ s},
        -- x : α, hx : x ∈ t
        -- goal : x ∈ s
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
⊢ x ∈ s
[PROOFSTEP]
have : x ∈ closure s := by
  refine' mem_closure_iff.2 fun ε εpos => _
  rcases mem_closure_iff.1 ht ε εpos with
    ⟨u, hu, Dtu⟩
      -- u : Closeds α, hu : u ∈ {t : Closeds α | t ⊆ s}, hu' : edist t u < ε
  rcases exists_edist_lt_of_hausdorffEdist_lt hx Dtu with
    ⟨y, hy, Dxy⟩
      -- y : α, hy : y ∈ u, Dxy : edist x y < ε
  exact ⟨y, hu hy, Dxy⟩
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
⊢ x ∈ closure s
[PROOFSTEP]
refine' mem_closure_iff.2 fun ε εpos => _
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y, y ∈ s ∧ edist x y < ε
[PROOFSTEP]
rcases mem_closure_iff.1 ht ε εpos with
  ⟨u, hu, Dtu⟩
    -- u : Closeds α, hu : u ∈ {t : Closeds α | t ⊆ s}, hu' : edist t u < ε
[GOAL]
case intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
⊢ ∃ y, y ∈ s ∧ edist x y < ε
[PROOFSTEP]
rcases exists_edist_lt_of_hausdorffEdist_lt hx Dtu with
  ⟨y, hy, Dxy⟩
    -- y : α, hy : y ∈ u, Dxy : edist x y < ε
[GOAL]
case intro.intro.intro.intro
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
ε : ℝ≥0∞
εpos : ε > 0
u : Closeds α
hu : u ∈ {t | ↑t ⊆ s}
Dtu : edist t u < ε
y : α
hy : y ∈ ↑u
Dxy : edist x y < ε
⊢ ∃ y, y ∈ s ∧ edist x y < ε
[PROOFSTEP]
exact ⟨y, hu hy, Dxy⟩
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s : Set α
hs : IsClosed s
t : Closeds α
ht : t ∈ closure {t | ↑t ⊆ s}
x : α
hx : x ∈ ↑t
this : x ∈ closure s
⊢ x ∈ s
[PROOFSTEP]
rwa [hs.closure_eq] at this 
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
⊢ CompleteSpace (Closeds α)
[PROOFSTEP]
let B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
⊢ CompleteSpace (Closeds α)
[PROOFSTEP]
have B_pos : ∀ n, (0 : ℝ≥0∞) < B n := by simp [ENNReal.pow_pos]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
⊢ ∀ (n : ℕ), 0 < B n
[PROOFSTEP]
simp [ENNReal.pow_pos]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
⊢ CompleteSpace (Closeds α)
[PROOFSTEP]
have B_ne_top : ∀ n, B n ≠ ⊤ := by
  simp [ENNReal.pow_ne_top]
    /- Consider a sequence of closed sets `s n` with `edist (s n) (s (n+1)) < B n`.
        We will show that it converges. The limit set is `t0 = ⋂n, closure (⋃m≥n, s m)`.
        We will have to show that a point in `s n` is close to a point in `t0`, and a point
        in `t0` is close to a point in `s n`. The completeness then follows from a
        standard criterion. -/
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
⊢ ∀ (n : ℕ), B n ≠ ⊤
[PROOFSTEP]
simp [ENNReal.pow_ne_top]
  /- Consider a sequence of closed sets `s n` with `edist (s n) (s (n+1)) < B n`.
      We will show that it converges. The limit set is `t0 = ⋂n, closure (⋃m≥n, s m)`.
      We will have to show that a point in `s n` is close to a point in `t0`, and a point
      in `t0` is close to a point in `s n`. The completeness then follows from a
      standard criterion. -/
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ⊤
⊢ CompleteSpace (Closeds α)
[PROOFSTEP]
refine' complete_of_convergent_controlled_sequences B B_pos fun s hs => _
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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
⊢ ∃ x, Tendsto s atTop (𝓝 x)
[PROOFSTEP]
let t0 := ⋂ n, closure (⋃ m ≥ n, s m : Set α)
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
⊢ ∃ x, Tendsto s atTop (𝓝 x)
[PROOFSTEP]
let t : Closeds α := ⟨t0, isClosed_iInter fun _ => isClosed_closure⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
⊢ ∃ x, Tendsto s atTop (𝓝 x)
[PROOFSTEP]
use t
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
⊢ Tendsto s atTop (𝓝 t)
[PROOFSTEP]
have I1 : ∀ n, ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n := by
  /- This is the main difficulty of the proof. Starting from `x ∈ s n`, we want
             to find a point in `t0` which is close to `x`. Define inductively a sequence of
             points `z m` with `z n = x` and `z m ∈ s m` and `edist (z m) (z (m+1)) ≤ B m`. This is
             possible since the Hausdorff distance between `s m` and `s (m+1)` is at most `B m`.
             This sequence is a Cauchy sequence, therefore converging as the space is complete, to
             a limit which satisfies the required properties. -/
  intro n x hx
  obtain ⟨z, hz₀, hz⟩ : ∃ z : ∀ l, s (n + l), (z 0 : α) = x ∧ ∀ k, edist (z k : α) (z (k + 1) : α) ≤ B n / 2 ^ k := by
    -- We prove existence of the sequence by induction.
    have : ∀ (l) (z : s (n + l)), ∃ z' : s (n + l + 1), edist (z : α) z' ≤ B n / 2 ^ l :=
      by
      intro l z
      obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l :=
        by
        refine' exists_edist_lt_of_hausdorffEdist_lt _ _
        · exact (s (n + l) : Set α)
        · exact z.2
        simp only [ENNReal.inv_pow, div_eq_mul_inv]
        rw [← pow_add]
        apply hs <;> simp
      exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩
    use fun k => Nat.recOn k ⟨x, hx⟩ fun l z => choose (this l z)
    simp only [Nat.add_zero, Nat.zero_eq, Nat.rec_zero, Nat.rec_add_one, true_and]
    exact fun k =>
      choose_spec
        (this k _)
          -- it follows from the previous bound that `z` is a Cauchy sequence
  have : CauchySeq fun k => (z k : α) := cauchySeq_of_edist_le_geometric_two (B n) (B_ne_top n) hz
  rcases cauchySeq_tendsto_of_complete this with ⟨y, y_lim⟩
  use y
  have : y ∈ t0 :=
    mem_iInter.2 fun k =>
      mem_closure_of_tendsto y_lim
        (by
          simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop, Set.mem_preimage, Set.preimage_iUnion]
          exact ⟨k, fun m hm => ⟨n + m, zero_add k ▸ add_le_add (zero_le n) hm, (z m).2⟩⟩)
  use this
  rw [← hz₀]
  exact edist_le_of_edist_le_geometric_two_of_tendsto₀ (B n) hz y_lim
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
⊢ ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
intro n x hx
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
⊢ ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
obtain ⟨z, hz₀, hz⟩ : ∃ z : ∀ l, s (n + l), (z 0 : α) = x ∧ ∀ k, edist (z k : α) (z (k + 1) : α) ≤ B n / 2 ^ k := by
  -- We prove existence of the sequence by induction.
  have : ∀ (l) (z : s (n + l)), ∃ z' : s (n + l + 1), edist (z : α) z' ≤ B n / 2 ^ l :=
    by
    intro l z
    obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l :=
      by
      refine' exists_edist_lt_of_hausdorffEdist_lt _ _
      · exact (s (n + l) : Set α)
      · exact z.2
      simp only [ENNReal.inv_pow, div_eq_mul_inv]
      rw [← pow_add]
      apply hs <;> simp
    exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩
  use fun k => Nat.recOn k ⟨x, hx⟩ fun l z => choose (this l z)
  simp only [Nat.add_zero, Nat.zero_eq, Nat.rec_zero, Nat.rec_add_one, true_and]
  exact fun k =>
    choose_spec
      (this k _)
        -- it follows from the previous bound that `z` is a Cauchy sequence
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
⊢ ∃ z, ↑(z 0) = x ∧ ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
[PROOFSTEP]
have : ∀ (l) (z : s (n + l)), ∃ z' : s (n + l + 1), edist (z : α) z' ≤ B n / 2 ^ l :=
  by
  intro l z
  obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l :=
    by
    refine' exists_edist_lt_of_hausdorffEdist_lt _ _
    · exact (s (n + l) : Set α)
    · exact z.2
    simp only [ENNReal.inv_pow, div_eq_mul_inv]
    rw [← pow_add]
    apply hs <;> simp
  exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
⊢ ∀ (l : ℕ) (z : { x // x ∈ s (n + l) }), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
[PROOFSTEP]
intro l z
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
[PROOFSTEP]
obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l :=
  by
  refine' exists_edist_lt_of_hausdorffEdist_lt _ _
  · exact (s (n + l) : Set α)
  · exact z.2
  simp only [ENNReal.inv_pow, div_eq_mul_inv]
  rw [← pow_add]
  apply hs <;> simp
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ ∃ z', z' ∈ s (n + l + 1) ∧ edist (↑z) z' < B n / 2 ^ l
[PROOFSTEP]
refine' exists_edist_lt_of_hausdorffEdist_lt _ _
[GOAL]
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ Set α
[PROOFSTEP]
exact (s (n + l) : Set α)
[GOAL]
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ ↑z ∈ ↑(s (n + l))
[PROOFSTEP]
exact z.2
[GOAL]
case refine'_3
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ hausdorffEdist ↑(s (n + l)) ↑(s (n + l + 1)) < B n / 2 ^ l
[PROOFSTEP]
simp only [ENNReal.inv_pow, div_eq_mul_inv]
[GOAL]
case refine'_3
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ hausdorffEdist ↑(s (n + l)) ↑(s (n + l + 1)) < 2⁻¹ ^ n * 2⁻¹ ^ l
[PROOFSTEP]
rw [← pow_add]
[GOAL]
case refine'_3
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ hausdorffEdist ↑(s (n + l)) ↑(s (n + l + 1)) < 2⁻¹ ^ (n + l)
[PROOFSTEP]
apply hs
[GOAL]
case refine'_3.a
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ n + l ≤ n + l
[PROOFSTEP]
simp
[GOAL]
case refine'_3.a
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
⊢ n + l ≤ n + l + 1
[PROOFSTEP]
simp
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : { x // x ∈ s (n + l) }
z' : α
z'_mem : z' ∈ s (n + l + 1)
hz' : edist (↑z) z' < B n / 2 ^ l
⊢ ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
[PROOFSTEP]
exact ⟨⟨z', z'_mem⟩, le_of_lt hz'⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
this : ∀ (l : ℕ) (z : { x // x ∈ s (n + l) }), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
⊢ ∃ z, ↑(z 0) = x ∧ ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
[PROOFSTEP]
use fun k => Nat.recOn k ⟨x, hx⟩ fun l z => choose (this l z)
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
this : ∀ (l : ℕ) (z : { x // x ∈ s (n + l) }), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
⊢ ↑(Nat.recOn 0 { val := x, property := hx } fun l z => choose (_ : ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l)) = x ∧
    ∀ (k : ℕ),
      edist ↑(Nat.recOn k { val := x, property := hx } fun l z => choose (_ : ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l))
          ↑(Nat.recOn (k + 1) { val := x, property := hx } fun l z => choose (_ : ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l)) ≤
        B n / 2 ^ k
[PROOFSTEP]
simp only [Nat.add_zero, Nat.zero_eq, Nat.rec_zero, Nat.rec_add_one, true_and]
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
this : ∀ (l : ℕ) (z : { x // x ∈ s (n + l) }), ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
⊢ ∀ (k : ℕ),
    edist ↑(Nat.rec { val := x, property := hx } (fun l z => choose (_ : ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l)) k)
        ↑(choose
            (_ :
              ∃ z',
                edist
                    ↑(Nat.rec { val := x, property := hx } (fun l z => choose (_ : ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l)) k)
                    ↑z' ≤
                  B n / 2 ^ k)) ≤
      2⁻¹ ^ n / 2 ^ k
[PROOFSTEP]
exact fun k =>
  choose_spec
    (this k _)
      -- it follows from the previous bound that `z` is a Cauchy sequence
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
⊢ ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
have : CauchySeq fun k => (z k : α) := cauchySeq_of_edist_le_geometric_two (B n) (B_ne_top n) hz
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k => ↑(z k)
⊢ ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
rcases cauchySeq_tendsto_of_complete this with ⟨y, y_lim⟩
[GOAL]
case intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
⊢ ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
use y
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
⊢ y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
have : y ∈ t0 :=
  mem_iInter.2 fun k =>
    mem_closure_of_tendsto y_lim
      (by
        simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop, Set.mem_preimage, Set.preimage_iUnion]
        exact ⟨k, fun m hm => ⟨n + m, zero_add k ▸ add_le_add (zero_le n) hm, (z m).2⟩⟩)
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
k : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(z x) ∈ ⋃ (m : ℕ) (_ : m ≥ k), ↑(s m)
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop, Set.mem_preimage, Set.preimage_iUnion]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
k : ℕ
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ∃ i, i ≥ k ∧ ↑(z b) ∈ ↑(s i)
[PROOFSTEP]
exact ⟨k, fun m hm => ⟨n + m, zero_add k ▸ add_le_add (zero_le n) hm, (z m).2⟩⟩
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this✝ : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
this : y ∈ t0
⊢ y ∈ t0 ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
use this
[GOAL]
case right
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this✝ : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
this : y ∈ t0
⊢ edist x y ≤ 2 * B n
[PROOFSTEP]
rw [← hz₀]
[GOAL]
case right
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → { x // x ∈ s (n + l) }
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this✝ : CauchySeq fun k => ↑(z k)
y : α
y_lim : Tendsto (fun k => ↑(z k)) atTop (𝓝 y)
this : y ∈ t0
⊢ edist (↑(z 0)) y ≤ 2 * B n
[PROOFSTEP]
exact edist_le_of_edist_le_geometric_two_of_tendsto₀ (B n) hz y_lim
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)
[PROOFSTEP]
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
  rcases mem_closure_iff.1 this (B n) (B_pos n) with
    ⟨z, hz, Dxz⟩
      -- z : α, Dxz : edist x z < B n,
  simp only [exists_prop, Set.mem_iUnion] at hz 
  rcases hz with
    ⟨m, ⟨m_ge_n, hm⟩⟩
      -- m : ℕ, m_ge_n : m ≥ n, hm : z ∈ s m
  have : hausdorffEdist (s m : Set α) (s n) < B n := hs n m n m_ge_n (le_refl n)
  rcases exists_edist_lt_of_hausdorffEdist_lt hm this with
    ⟨y, hy, Dzy⟩
      -- y : α, hy : y ∈ s n, Dzy : edist z y < B n
  exact
    ⟨y, hy,
      calc
        edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
        _ ≤ B n + B n := (add_le_add (le_of_lt Dxz) (le_of_lt Dzy))
        _ = 2 * B n := (two_mul _).symm⟩
      -- Deduce from the above inequalities that the distance between `s n` and `t0` is at most `2 B n`.
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
⊢ ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
intro n x xt0
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
have : x ∈ closure (⋃ m ≥ n, s m : Set α) := by apply mem_iInter.1 xt0 n
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
⊢ x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
[PROOFSTEP]
apply mem_iInter.1 xt0 n
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this : x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
rcases mem_closure_iff.1 this (B n) (B_pos n) with
  ⟨z, hz, Dxz⟩
    -- z : α, Dxz : edist x z < B n,
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this : x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
z : α
hz : z ∈ ⋃ (m : ℕ) (_ : m ≥ n), ↑(s m)
Dxz : edist x z < B n
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion] at hz 
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this : x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
z : α
Dxz : edist x z < B n
hz : ∃ i, i ≥ n ∧ z ∈ ↑(s i)
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
rcases hz with
  ⟨m, ⟨m_ge_n, hm⟩⟩
    -- m : ℕ, m_ge_n : m ≥ n, hm : z ∈ s m
[GOAL]
case intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this : x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
z : α
Dxz : edist x z < B n
m : ℕ
m_ge_n : m ≥ n
hm : z ∈ ↑(s m)
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
have : hausdorffEdist (s m : Set α) (s n) < B n := hs n m n m_ge_n (le_refl n)
[GOAL]
case intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this✝ : x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
z : α
Dxz : edist x z < B n
m : ℕ
m_ge_n : m ≥ n
hm : z ∈ ↑(s m)
this : hausdorffEdist ↑(s m) ↑(s n) < B n
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
rcases exists_edist_lt_of_hausdorffEdist_lt hm this with
  ⟨y, hy, Dzy⟩
    -- y : α, hy : y ∈ s n, Dzy : edist z y < B n
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this✝ : x ∈ closure (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
z : α
Dxz : edist x z < B n
m : ℕ
m_ge_n : m ≥ n
hm : z ∈ ↑(s m)
this : hausdorffEdist ↑(s m) ↑(s n) < B n
y : α
hy : y ∈ ↑(s n)
Dzy : edist z y < B n
⊢ ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
[PROOFSTEP]
exact
  ⟨y, hy,
    calc
      edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
      _ ≤ B n + B n := (add_le_add (le_of_lt Dxz) (le_of_lt Dzy))
      _ = 2 * B n := (two_mul _).symm⟩
    -- Deduce from the above inequalities that the distance between `s n` and `t0` is at most `2 B n`.
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)
[PROOFSTEP]
have main : ∀ n : ℕ, edist (s n) t ≤ 2 * B n := fun n =>
  hausdorffEdist_le_of_mem_edist (I1 n)
    (I2 n)
      -- from this, the convergence of `s n` to `t0` follows.
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)
[PROOFSTEP]
refine' tendsto_atTop.2 fun ε εpos => _
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → edist (s n) t < ε
[PROOFSTEP]
have : Tendsto (fun n => 2 * B n) atTop (𝓝 (2 * 0)) :=
  ENNReal.Tendsto.const_mul (ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 <| by simp [ENNReal.one_lt_two])
    (Or.inr <| by simp)
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
⊢ 2⁻¹ < 1
[PROOFSTEP]
simp [ENNReal.one_lt_two]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, y ∈ s n ∧ edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
⊢ 2 ≠ ⊤
[PROOFSTEP]
simp
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, 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 (𝓝 (2 * 0))
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → edist (s n) t < ε
[PROOFSTEP]
rw [mul_zero] at this 
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, 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 (𝓝 0)
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → edist (s n) t < ε
[PROOFSTEP]
obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b := ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop
[GOAL]
case h.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n => 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 (⋃ (m : ℕ) (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, closed' := (_ : IsClosed (⋂ (i : ℕ), closure (⋃ (m : ℕ) (_ : m ≥ i), ↑(s m)))) }
I1 : ∀ (n : ℕ) (x : α), x ∈ s n → ∃ y, y ∈ t0 ∧ edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ) (x : α), x ∈ t0 → ∃ y, 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 (𝓝 0)
N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ε > 2 * B b
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → edist (s n) t < ε
[PROOFSTEP]
exact ⟨N, fun n hn => lt_of_le_of_lt (main n) (hN n hn)⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompactSpace α
⊢ IsCompact univ
[PROOFSTEP]
refine' isCompact_of_totallyBounded_isClosed (EMetric.totallyBounded_iff.2 fun ε εpos => _) isClosed_univ
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ t, Set.Finite t ∧ univ ⊆ ⋃ (y : Closeds α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
rcases exists_between εpos with ⟨δ, δpos, δlt⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
⊢ ∃ t, Set.Finite t ∧ univ ⊆ ⋃ (y : Closeds α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
rcases EMetric.totallyBounded_iff.1 (isCompact_iff_totallyBounded_isComplete.1 (@isCompact_univ α _ _)).1 δ δpos with
  ⟨s, fs, hs⟩
    -- s : Set α, fs : s.Finite, hs : univ ⊆ ⋃ (y : α) (H : y ∈ s), eball y δ
        -- we first show that any set is well approximated by a subset of `s`.
[GOAL]
case intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
⊢ ∃ t, Set.Finite t ∧ univ ⊆ ⋃ (y : Closeds α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
have main : ∀ u : Set α, ∃ (v : _) (_ : v ⊆ s), hausdorffEdist u v ≤ δ :=
  by
  intro u
  let v := {x : α | x ∈ s ∧ ∃ y ∈ u, edist x y < δ}
  exists v, (fun x hx => hx.1 : v ⊆ s)
  refine' hausdorffEdist_le_of_mem_edist _ _
  · intro x hx
    have : x ∈ ⋃ y ∈ s, ball y δ := hs (by simp)
    rcases mem_iUnion₂.1 this with ⟨y, ys, dy⟩
    have : edist y x < δ := by simp at dy ; rwa [edist_comm] at dy 
    exact ⟨y, ⟨ys, ⟨x, hx, this⟩⟩, le_of_lt dy⟩
  · rintro x ⟨_, ⟨y, yu, hy⟩⟩
    exact
      ⟨y, yu, le_of_lt hy⟩
        -- introduce the set F of all subsets of `s` (seen as members of `Closeds α`).
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
⊢ ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
[PROOFSTEP]
intro u
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
⊢ ∃ v x, hausdorffEdist u v ≤ δ
[PROOFSTEP]
let v := {x : α | x ∈ s ∧ ∃ y ∈ u, edist x y < δ}
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
⊢ ∃ v x, hausdorffEdist u v ≤ δ
[PROOFSTEP]
exists v, (fun x hx => hx.1 : v ⊆ s)
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
⊢ hausdorffEdist u v ≤ δ
[PROOFSTEP]
refine' hausdorffEdist_le_of_mem_edist _ _
[GOAL]
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
⊢ ∀ (x : α), x ∈ u → ∃ y, y ∈ v ∧ edist x y ≤ δ
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
⊢ ∃ y, y ∈ v ∧ edist x y ≤ δ
[PROOFSTEP]
have : x ∈ ⋃ y ∈ s, ball y δ := hs (by simp)
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
⊢ x ∈ univ
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
this : x ∈ ⋃ (y : α) (_ : y ∈ s), ball y δ
⊢ ∃ y, y ∈ v ∧ edist x y ≤ δ
[PROOFSTEP]
rcases mem_iUnion₂.1 this with ⟨y, ys, dy⟩
[GOAL]
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
this : x ∈ ⋃ (y : α) (_ : y ∈ s), ball y δ
y : α
ys : y ∈ s
dy : x ∈ ball y δ
⊢ ∃ y, y ∈ v ∧ edist x y ≤ δ
[PROOFSTEP]
have : edist y x < δ := by simp at dy ; rwa [edist_comm] at dy 
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
this : x ∈ ⋃ (y : α) (_ : y ∈ s), ball y δ
y : α
ys : y ∈ s
dy : x ∈ ball y δ
⊢ edist y x < δ
[PROOFSTEP]
simp at dy 
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
this : x ∈ ⋃ (y : α) (_ : y ∈ s), ball y δ
y : α
ys : y ∈ s
dy : edist x y < δ
⊢ edist y x < δ
[PROOFSTEP]
rwa [edist_comm] at dy 
[GOAL]
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
hx : x ∈ u
this✝ : x ∈ ⋃ (y : α) (_ : y ∈ s), ball y δ
y : α
ys : y ∈ s
dy : x ∈ ball y δ
this : edist y x < δ
⊢ ∃ y, y ∈ v ∧ edist x y ≤ δ
[PROOFSTEP]
exact ⟨y, ⟨ys, ⟨x, hx, this⟩⟩, le_of_lt dy⟩
[GOAL]
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
⊢ ∀ (x : α), x ∈ v → ∃ y, y ∈ u ∧ edist x y ≤ δ
[PROOFSTEP]
rintro x ⟨_, ⟨y, yu, hy⟩⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
u : Set α
v : Set α := {x | x ∈ s ∧ ∃ y, y ∈ u ∧ edist x y < δ}
x : α
left✝ : x ∈ s
y : α
yu : y ∈ u
hy : edist x y < δ
⊢ ∃ y, y ∈ u ∧ edist x y ≤ δ
[PROOFSTEP]
exact
  ⟨y, yu, le_of_lt hy⟩
    -- introduce the set F of all subsets of `s` (seen as members of `Closeds α`).
[GOAL]
case intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
⊢ ∃ t, Set.Finite t ∧ univ ⊆ ⋃ (y : Closeds α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
let F := {f : Closeds α | (f : Set α) ⊆ s}
[GOAL]
case intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ ∃ t, Set.Finite t ∧ univ ⊆ ⋃ (y : Closeds α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
refine'
  ⟨F, _, fun u _ => _⟩
    -- `F` is finite
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ Set.Finite F
[PROOFSTEP]
apply @Finite.of_finite_image _ _ F _
[GOAL]
case intro.intro.intro.intro.refine'_1.h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ Set.Finite (?m.23554 '' F)
[PROOFSTEP]
apply fs.finite_subsets.subset fun b => _
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ Closeds α → Set α
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ ∀ (b : Set α), b ∈ ?m.23554 '' F → b ∈ {b | b ⊆ s}
[PROOFSTEP]
exact fun s => (s : Set α)
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ ∀ (b : Set α), b ∈ (fun s => ↑s) '' F → b ∈ {b | b ⊆ s}
[PROOFSTEP]
simp only [and_imp, Set.mem_image, Set.mem_setOf_eq, exists_imp]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ ∀ (b : Set α) (x : Closeds α), ↑x ⊆ s → ↑x = b → b ⊆ s
[PROOFSTEP]
intro _ x hx hx'
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
b✝ : Set α
x : Closeds α
hx : ↑x ⊆ s
hx' : ↑x = b✝
⊢ b✝ ⊆ s
[PROOFSTEP]
rwa [hx'] at hx 
[GOAL]
case intro.intro.intro.intro.refine'_1.hi
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
⊢ InjOn (fun s => ↑s) F
[PROOFSTEP]
exact SetLike.coe_injective.injOn F
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
⊢ u ∈ ⋃ (y : Closeds α) (_ : y ∈ F), ball y ε
[PROOFSTEP]
obtain ⟨t0, t0s, Dut0⟩ := main u
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
t0 : Set α
t0s : t0 ⊆ s
Dut0 : hausdorffEdist (↑u) t0 ≤ δ
⊢ u ∈ ⋃ (y : Closeds α) (_ : y ∈ F), ball y ε
[PROOFSTEP]
have : IsClosed t0 := (fs.subset t0s).isCompact.isClosed
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
t0 : Set α
t0s : t0 ⊆ s
Dut0 : hausdorffEdist (↑u) t0 ≤ δ
this : IsClosed t0
⊢ u ∈ ⋃ (y : Closeds α) (_ : y ∈ F), ball y ε
[PROOFSTEP]
let t : Closeds α := ⟨t0, this⟩
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
t0 : Set α
t0s : t0 ⊆ s
Dut0 : hausdorffEdist (↑u) t0 ≤ δ
this : IsClosed t0
t : Closeds α := { carrier := t0, closed' := this }
⊢ u ∈ ⋃ (y : Closeds α) (_ : y ∈ F), ball y ε
[PROOFSTEP]
have : t ∈ F := t0s
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
t0 : Set α
t0s : t0 ⊆ s
Dut0 : hausdorffEdist (↑u) t0 ≤ δ
this✝ : IsClosed t0
t : Closeds α := { carrier := t0, closed' := this✝ }
this : t ∈ F
⊢ u ∈ ⋃ (y : Closeds α) (_ : y ∈ F), ball y ε
[PROOFSTEP]
have : edist u t < ε := lt_of_le_of_lt Dut0 δlt
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
t0 : Set α
t0s : t0 ⊆ s
Dut0 : hausdorffEdist (↑u) t0 ≤ δ
this✝¹ : IsClosed t0
t : Closeds α := { carrier := t0, closed' := this✝¹ }
this✝ : t ∈ F
this : edist u t < ε
⊢ u ∈ ⋃ (y : Closeds α) (_ : y ∈ F), ball y ε
[PROOFSTEP]
apply mem_iUnion₂.2
[GOAL]
case intro.intro.intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompactSpace α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
s : Set α
fs : Set.Finite s
hs : univ ⊆ ⋃ (y : α) (_ : y ∈ s), ball y δ
main : ∀ (u : Set α), ∃ v x, hausdorffEdist u v ≤ δ
F : Set (Closeds α) := {f | ↑f ⊆ s}
u : Closeds α
x✝ : u ∈ univ
t0 : Set α
t0s : t0 ⊆ s
Dut0 : hausdorffEdist (↑u) t0 ≤ δ
this✝¹ : IsClosed t0
t : Closeds α := { carrier := t0, closed' := this✝¹ }
this✝ : t ∈ F
this : edist u t < ε
⊢ ∃ i j, u ∈ ball i ε
[PROOFSTEP]
exact ⟨t, ‹t ∈ F›, this⟩
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
⊢ ↑s = ↑t
[PROOFSTEP]
have : closure (s : Set α) = closure t := hausdorffEdist_zero_iff_closure_eq_closure.1 h
[GOAL]
α : Type u
inst✝ : EMetricSpace α
s✝ : Set α
s t : NonemptyCompacts α
h : edist s t = 0
this : closure ↑s = closure ↑t
⊢ ↑s = ↑t
[PROOFSTEP]
rwa [s.isCompact.isClosed.closure_eq, t.isCompact.isClosed.closure_eq] at this 
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
⊢ IsClosed (range NonemptyCompacts.toCloseds)
[PROOFSTEP]
have : range NonemptyCompacts.toCloseds = {s : Closeds α | (s : Set α).Nonempty ∧ IsCompact (s : Set α)} :=
  by
  ext s
  refine' ⟨_, fun h => ⟨⟨⟨s, h.2⟩, h.1⟩, Closeds.ext rfl⟩⟩
  rintro ⟨s, hs, rfl⟩
  exact ⟨s.nonempty, s.isCompact⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
⊢ range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
[PROOFSTEP]
ext s
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds ↔ s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
[PROOFSTEP]
refine' ⟨_, fun h => ⟨⟨⟨s, h.2⟩, h.1⟩, Closeds.ext rfl⟩⟩
[GOAL]
case h
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : Closeds α
⊢ s ∈ range NonemptyCompacts.toCloseds → s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
[PROOFSTEP]
rintro ⟨s, hs, rfl⟩
[GOAL]
case h.intro.refl
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
s : NonemptyCompacts α
⊢ NonemptyCompacts.toCloseds s ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
[PROOFSTEP]
exact ⟨s.nonempty, s.isCompact⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsClosed (range NonemptyCompacts.toCloseds)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsClosed {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
[PROOFSTEP]
refine' isClosed_of_closure_subset fun s hs => ⟨_, _⟩
[GOAL]
case refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ Set.Nonempty ↑s
[PROOFSTEP]
rcases mem_closure_iff.1 hs ⊤ ENNReal.coe_lt_top with ⟨t, ht, Dst⟩
[GOAL]
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ⊤
⊢ Set.Nonempty ↑s
[PROOFSTEP]
rw [edist_comm] at Dst 
[GOAL]
case refine'_1.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist t s < ⊤
⊢ Set.Nonempty ↑s
[PROOFSTEP]
exact nonempty_of_hausdorffEdist_ne_top ht.1 (ne_of_lt Dst)
[GOAL]
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ IsCompact ↑s
[PROOFSTEP]
refine' isCompact_iff_totallyBounded_isComplete.2 ⟨_, s.closed.isComplete⟩
[GOAL]
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
⊢ TotallyBounded ↑s
[PROOFSTEP]
refine'
  totallyBounded_iff.2 fun ε (εpos : 0 < ε) =>
    _
      -- we have to show that s is covered by finitely many eballs of radius ε
          -- pick a nonempty compact set t at distance at most ε/2 of s
[GOAL]
case refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
rcases mem_closure_iff.1 hs (ε / 2) (ENNReal.half_pos εpos.ne') with
  ⟨t, ht, Dst⟩
    -- cover this space with finitely many balls of radius ε/2
[GOAL]
case refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
rcases totallyBounded_iff.1 (isCompact_iff_totallyBounded_isComplete.1 ht.2).1 (ε / 2) (ENNReal.half_pos εpos.ne') with
  ⟨u, fu, ut⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
⊢ ∃ t, Set.Finite t ∧ ↑s ⊆ ⋃ (y : α) (_ : y ∈ t), ball y ε
[PROOFSTEP]
refine'
  ⟨u, ⟨fu, fun x hx => _⟩⟩
    -- u : set α, fu : u.finite, ut : t ⊆ ⋃ (y : α) (H : y ∈ u), eball y (ε / 2)
        -- then s is covered by the union of the balls centered at u of radius ε
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
[PROOFSTEP]
rcases exists_edist_lt_of_hausdorffEdist_lt hx Dst with ⟨z, hz, Dxz⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
[PROOFSTEP]
rcases mem_iUnion₂.1 (ut hz) with ⟨y, hy, Dzy⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
[PROOFSTEP]
have : edist x y < ε :=
  calc
    edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
    _ < ε / 2 + ε / 2 := (ENNReal.add_lt_add Dxz Dzy)
    _ = ε := ENNReal.add_halves _
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : CompleteSpace α
this✝ : range NonemptyCompacts.toCloseds = {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
s : Closeds α
hs : s ∈ closure {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
ε : ℝ≥0∞
εpos : 0 < ε
t : Closeds α
ht : t ∈ {s | Set.Nonempty ↑s ∧ IsCompact ↑s}
Dst : edist s t < ε / 2
u : Set α
fu : Set.Finite u
ut : ↑t ⊆ ⋃ (y : α) (_ : y ∈ u), ball y (ε / 2)
x : α
hx : x ∈ ↑s
z : α
hz : z ∈ ↑t
Dxz : edist x z < ε / 2
y : α
hy : y ∈ u
Dzy : z ∈ ball y (ε / 2)
this : edist x y < ε
⊢ x ∈ ⋃ (y : α) (_ : y ∈ u), ball y ε
[PROOFSTEP]
exact mem_biUnion hy this
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompactSpace α
⊢ IsCompact univ
[PROOFSTEP]
rw [NonemptyCompacts.ToCloseds.uniformEmbedding.embedding.isCompact_iff_isCompact_image]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompactSpace α
⊢ IsCompact (NonemptyCompacts.toCloseds '' univ)
[PROOFSTEP]
rw [image_univ]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : CompactSpace α
⊢ IsCompact (range NonemptyCompacts.toCloseds)
[PROOFSTEP]
exact NonemptyCompacts.isClosed_in_closeds.isCompact
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : SecondCountableTopology α
⊢ SeparableSpace (NonemptyCompacts α)
[PROOFSTEP]
rcases exists_countable_dense α with ⟨s, cs, s_dense⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
⊢ SeparableSpace (NonemptyCompacts α)
[PROOFSTEP]
let v0 := {t : Set α | t.Finite ∧ t ⊆ s}
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
⊢ SeparableSpace (NonemptyCompacts α)
[PROOFSTEP]
let v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (t : Set α) ∈ v0}
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
⊢ SeparableSpace (NonemptyCompacts α)
[PROOFSTEP]
refine' ⟨⟨v, _, _⟩⟩
[GOAL]
case intro.intro.refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
⊢ Set.Countable v
[PROOFSTEP]
have : v0.Countable := countable_setOf_finite_subset cs
[GOAL]
case intro.intro.refine'_1
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
this : Set.Countable v0
⊢ Set.Countable v
[PROOFSTEP]
exact this.preimage SetLike.coe_injective
[GOAL]
case intro.intro.refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
⊢ Dense v
[PROOFSTEP]
refine' fun t =>
  mem_closure_iff.2 fun ε εpos =>
    _
      -- t is a compact nonempty set, that we have to approximate uniformly by a a set in `v`.
[GOAL]
case intro.intro.refine'_2
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
rcases exists_between εpos with ⟨δ, δpos, δlt⟩
[GOAL]
case intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have δpos' : 0 < δ / 2 := ENNReal.half_pos δpos.ne'
[GOAL]
case intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have Exy : ∀ x, ∃ y, y ∈ s ∧ edist x y < δ / 2 := by
  intro x
  rcases mem_closure_iff.1 (s_dense x) (δ / 2) δpos' with ⟨y, ys, hy⟩
  exact ⟨y, ⟨ys, hy⟩⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
⊢ ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
[PROOFSTEP]
intro x
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
x : α
⊢ ∃ y, y ∈ s ∧ edist x y < δ / 2
[PROOFSTEP]
rcases mem_closure_iff.1 (s_dense x) (δ / 2) δpos' with ⟨y, ys, hy⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
x y : α
ys : y ∈ s
hy : edist x y < δ / 2
⊢ ∃ y, y ∈ s ∧ edist x y < δ / 2
[PROOFSTEP]
exact ⟨y, ⟨ys, hy⟩⟩
[GOAL]
case intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
let F x := choose (Exy x)
[GOAL]
case intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have Fspec : ∀ x, F x ∈ s ∧ edist x (F x) < δ / 2 := fun x =>
  choose_spec
    (Exy x)
      -- cover `t` with finitely many balls. Their centers form a set `a`
[GOAL]
case intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have : TotallyBounded (t : Set α) := t.isCompact.totallyBounded
[GOAL]
case intro.intro.refine'_2.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this : TotallyBounded ↑t
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
rcases totallyBounded_iff.1 this (δ / 2) δpos' with
  ⟨a, af, ta⟩
    -- a : set α, af : a.finite, ta : t ⊆ ⋃ (y : α) (H : y ∈ a), eball y (δ / 2)
          -- replace each center by a nearby approximation in `s`, giving a new set `b`
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
let b := F '' a
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have : b.Finite := af.image _
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
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
        _
          -- keep only the points in `b` that are close to point in `t`, yielding a new set `c`
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
x : α
hx : x ∈ t
⊢ ∃ y, y ∈ b ∧ edist x y < δ
[PROOFSTEP]
rcases mem_iUnion₂.1 (ta hx) with ⟨z, za, Dxz⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
x : α
hx : x ∈ t
z : α
za : z ∈ a
Dxz : x ∈ ball z (δ / 2)
⊢ ∃ y, y ∈ b ∧ edist x y < δ
[PROOFSTEP]
exists F z, mem_image_of_mem _ za
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
x : α
hx : x ∈ t
z : α
za : z ∈ a
Dxz : x ∈ ball z (δ / 2)
⊢ edist x (F z) < δ
[PROOFSTEP]
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
      _
        -- keep only the points in `b` that are close to point in `t`, yielding a new set `c`
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
let c := {y ∈ b | ∃ x ∈ t, edist x y < δ}
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have : c.Finite :=
  ‹b.Finite›.subset fun x hx =>
    hx.1
      -- points in `t` are well approximated by points in `c`
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ := by
  intro x hx
  rcases tb x hx with ⟨y, yv, Dxy⟩
  have : y ∈ c := by simp [-mem_image]; exact ⟨yv, ⟨x, hx, Dxy⟩⟩
  exact
    ⟨y, this, le_of_lt Dxy⟩
      -- points in `c` are well approximated by points in `t`
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
⊢ ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
x : α
hx : x ∈ t
⊢ ∃ y, y ∈ c ∧ edist x y ≤ δ
[PROOFSTEP]
rcases tb x hx with ⟨y, yv, Dxy⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
x : α
hx : x ∈ t
y : α
yv : y ∈ b
Dxy : edist x y < δ
⊢ ∃ y, y ∈ c ∧ edist x y ≤ δ
[PROOFSTEP]
have : y ∈ c := by simp [-mem_image]; exact ⟨yv, ⟨x, hx, Dxy⟩⟩
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
x : α
hx : x ∈ t
y : α
yv : y ∈ b
Dxy : edist x y < δ
⊢ y ∈ c
[PROOFSTEP]
simp [-mem_image]
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
x : α
hx : x ∈ t
y : α
yv : y ∈ b
Dxy : edist x y < δ
⊢ y ∈ (fun a => choose (_ : ∃ y, y ∈ s ∧ edist a y < δ / 2)) '' a ∧ ∃ x, x ∈ t ∧ edist x y < δ
[PROOFSTEP]
exact ⟨yv, ⟨x, hx, Dxy⟩⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
x : α
hx : x ∈ t
y : α
yv : y ∈ b
Dxy : edist x y < δ
this : y ∈ c
⊢ ∃ y, y ∈ c ∧ edist x y ≤ δ
[PROOFSTEP]
exact
  ⟨y, this, le_of_lt Dxy⟩
    -- points in `c` are well approximated by points in `t`
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ := by
  rintro y ⟨_, x, xt, Dyx⟩
  have : edist y x ≤ δ :=
    calc
      edist y x = edist x y := edist_comm _ _
      _ ≤ δ := le_of_lt Dyx
  exact
    ⟨x, xt, this⟩
      -- it follows that their Hausdorff distance is small
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
⊢ ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
[PROOFSTEP]
rintro y ⟨_, x, xt, Dyx⟩
[GOAL]
case intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
y : α
left✝ : y ∈ b
x : α
xt : x ∈ t
Dyx : edist x y < δ
⊢ ∃ x, x ∈ t ∧ edist y x ≤ δ
[PROOFSTEP]
have : edist y x ≤ δ :=
  calc
    edist y x = edist x y := edist_comm _ _
    _ ≤ δ := le_of_lt Dyx
[GOAL]
case intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
y : α
left✝ : y ∈ b
x : α
xt : x ∈ t
Dyx : edist x y < δ
this : edist y x ≤ δ
⊢ ∃ x, x ∈ t ∧ edist y x ≤ δ
[PROOFSTEP]
exact
  ⟨x, xt, this⟩
    -- it follows that their Hausdorff distance is small
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝¹ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have : hausdorffEdist (t : Set α) c ≤ δ := hausdorffEdist_le_of_mem_edist tc ct
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have Dtc : hausdorffEdist (t : Set α) c < ε := this.trans_lt δlt
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have hc : c.Nonempty :=
  nonempty_of_hausdorffEdist_ne_top t.nonempty
    (ne_top_of_lt Dtc)
      -- let `d` be the version of `c` in the type `NonemptyCompacts α`
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
let d : NonemptyCompacts α := ⟨⟨c, ‹c.Finite›.isCompact⟩, hc⟩
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have : c ⊆ s := by
  intro x hx
  rcases(mem_image _ _ _).1 hx.1 with ⟨y, ⟨_, yx⟩⟩
  rw [← yx]
  exact (Fspec y).1
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
⊢ c ⊆ s
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
x : α
hx : x ∈ c
⊢ x ∈ s
[PROOFSTEP]
rcases(mem_image _ _ _).1 hx.1 with ⟨y, ⟨_, yx⟩⟩
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
x : α
hx : x ∈ c
y : α
left✝ : y ∈ a
yx : F y = x
⊢ x ∈ s
[PROOFSTEP]
rw [← yx]
[GOAL]
case intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝² : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝¹ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
x : α
hx : x ∈ c
y : α
left✝ : y ∈ a
yx : F y = x
⊢ F y ∈ s
[PROOFSTEP]
exact (Fspec y).1
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝³ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝² : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝¹ : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this✝ : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
this : c ⊆ s
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
have : d ∈ v :=
  ⟨‹c.Finite›, this⟩
    -- we have proved that `d` is a good approximation of `t` as requested
[GOAL]
case intro.intro.refine'_2.intro.intro.intro.intro
α : Type u
inst✝¹ : EMetricSpace α
s✝ : Set α
inst✝ : SecondCountableTopology α
s : Set α
cs : Set.Countable s
s_dense : Dense s
v0 : Set (Set α) := {t | Set.Finite t ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t | ↑t ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y, y ∈ s ∧ edist x y < δ / 2
F : α → α := fun x => choose (_ : ∃ y, y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this✝⁴ : TotallyBounded ↑t
a : Set α
af : Set.Finite a
ta : ↑t ⊆ ⋃ (y : α) (_ : y ∈ a), ball y (δ / 2)
b : Set α := F '' a
this✝³ : Set.Finite b
tb : ∀ (x : α), x ∈ t → ∃ y, y ∈ b ∧ edist x y < δ
c : Set α := {y | y ∈ b ∧ ∃ x, x ∈ t ∧ edist x y < δ}
this✝² : Set.Finite c
tc : ∀ (x : α), x ∈ t → ∃ y, y ∈ c ∧ edist x y ≤ δ
ct : ∀ (y : α), y ∈ c → ∃ x, x ∈ t ∧ edist y x ≤ δ
this✝¹ : hausdorffEdist (↑t) c ≤ δ
Dtc : hausdorffEdist (↑t) c < ε
hc : Set.Nonempty c
d : NonemptyCompacts α := { toCompacts := { carrier := c, isCompact' := (_ : IsCompact c) }, nonempty' := hc }
this✝ : c ⊆ s
this : d ∈ v
⊢ ∃ y, y ∈ v ∧ edist t y < ε
[PROOFSTEP]
exact ⟨d, ‹d ∈ v›, Dtc⟩
[GOAL]
α : Type u
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist s t
[PROOFSTEP]
rw [dist_comm]
[GOAL]
α : Type u
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist t s
[PROOFSTEP]
exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)
[GOAL]
α : Type u
inst✝ : MetricSpace α
⊢ LipschitzWith 2 fun p => infDist p.fst ↑p.snd
[PROOFSTEP]
convert
  @LipschitzWith.uncurry α (NonemptyCompacts α) ℝ _ _ _ (fun (x : α) (s : NonemptyCompacts α) => infDist x s) 1 1
    (fun s => lipschitz_infDist_pt ↑s) lipschitz_infDist_set
[GOAL]
case h.e'_5
α : Type u
inst✝ : MetricSpace α
⊢ 2 = 1 + 1
[PROOFSTEP]
norm_num
