[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ParacompactSpace α
[PROOFSTEP]
have pow_pos : ∀ k : ℕ, (0 : ℝ≥0∞) < 2⁻¹ ^ k := fun k => ENNReal.pow_pos (ENNReal.inv_pos.2 ENNReal.two_ne_top) _
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
⊢ ParacompactSpace α
[PROOFSTEP]
have hpow_le : ∀ {m n : ℕ}, m ≤ n → (2⁻¹ : ℝ≥0∞) ^ n ≤ 2⁻¹ ^ m :=
  @fun m n h => pow_le_pow_of_le_one' (ENNReal.inv_le_one.2 ENNReal.one_lt_two.le) h
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
⊢ ParacompactSpace α
[PROOFSTEP]
have h2pow : ∀ n : ℕ, 2 * (2⁻¹ : ℝ≥0∞) ^ (n + 1) = 2⁻¹ ^ n := fun n => by
  simp [pow_succ, ← mul_assoc, ENNReal.mul_inv_cancel]
    -- Consider an open covering `S : Set (Set α)`
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
n : ℕ
⊢ 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
[PROOFSTEP]
simp [pow_succ, ← mul_assoc, ENNReal.mul_inv_cancel]
  -- Consider an open covering `S : Set (Set α)`
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
⊢ ParacompactSpace α
[PROOFSTEP]
refine' ⟨fun ι s ho hcov => _⟩
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ⋃ (a : ι), s a = univ
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
simp only [iUnion_eq_univ_iff] at hcov
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
let _ : LinearOrder ι := by classical exact linearOrderOfSTO WellOrderingRel
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
⊢ LinearOrder ι
[PROOFSTEP]
classical exact linearOrderOfSTO WellOrderingRel
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
⊢ LinearOrder ι
[PROOFSTEP]
exact linearOrderOfSTO WellOrderingRel
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have wf : WellFounded ((· < ·) : ι → ι → Prop) :=
  @IsWellFounded.wf ι WellOrderingRel
    _
      -- Let `ind x` be the minimal index `s : S` such that `x ∈ s`.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
set ind : α → ι := fun x => wf.min {i : ι | x ∈ s i} (hcov x)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have mem_ind : ∀ x, x ∈ s (ind x) := fun x => wf.min_mem _ (hcov x)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have nmem_of_lt_ind : ∀ {x i}, i < ind x → x ∉ s i := @fun x i hlt hxi => wf.not_lt_min _ (hcov x) hxi hlt
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
set D : ℕ → ι → Set α := fun n =>
  Nat.strongRecOn' n fun n D' i =>
    ⋃ (x : α) (hxs : ind x = i) (hb : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (hlt :
      ∀ (m : ℕ) (H : m < n), ∀ (j : ι), x ∉ D' m H j), ball x (2⁻¹ ^ n) with
  hD
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have Dn :
  ∀ n i,
    D n i =
      ⋃ (x : α) (hxs : ind x = i) (hb : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (hlt : ∀ m < n, ∀ (j : ι), x ∉ D m j),
        ball x (2⁻¹ ^ n) :=
  fun n s => by
  simp only [hD]
  rw [Nat.strongRecOn'_beta]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s✝ : ι → Set α
ho : ∀ (a : ι), IsOpen (s✝ a)
hcov : ∀ (x : α), ∃ i, x ∈ s✝ i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s✝ i} (_ : ∃ i, x ∈ s✝ i)
mem_ind : ∀ (x : α), x ∈ s✝ (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s✝ i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
n : ℕ
s : ι
⊢ D n s =
    ⋃ (x : α) (_ : ind x = s) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ s) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
      ball x (2⁻¹ ^ n)
[PROOFSTEP]
simp only [hD]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s✝ : ι → Set α
ho : ∀ (a : ι), IsOpen (s✝ a)
hcov : ∀ (x : α), ∃ i, x ∈ s✝ i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s✝ i} (_ : ∃ i, x ∈ s✝ i)
mem_ind : ∀ (x : α), x ∈ s✝ (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s✝ i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
n : ℕ
s : ι
⊢ Nat.strongRecOn' n
      (fun n D' i =>
        ⋃ (x : α) (_ : WellFounded.min wf {i | x ∈ s✝ i} (_ : ∃ i, x ∈ s✝ i) = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ i) (_ :
          ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j), ball x (2⁻¹ ^ n))
      s =
    ⋃ (x : α) (_ : WellFounded.min wf {i | x ∈ s✝ i} (_ : ∃ i, x ∈ s✝ i) = s) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s✝ s) (_ :
      ∀ (m : ℕ),
        m < n →
          ∀ (j : ι),
            ¬x ∈
                Nat.strongRecOn' m
                  (fun n D' i =>
                    ⋃ (x : α) (_ : WellFounded.min wf {i | x ∈ s✝ i} (_ : ∃ i, x ∈ s✝ i) = i) (_ :
                      ball x (3 * 2⁻¹ ^ n) ⊆ s✝ i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j), ball x (2⁻¹ ^ n))
                  j),
      ball x (2⁻¹ ^ n)
[PROOFSTEP]
rw [Nat.strongRecOn'_beta]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have memD :
  ∀ {n i y},
    y ∈ D n i ↔
      ∃ x : α, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n :=
  by
  intro n i y
  rw [Dn n i]
  simp only [mem_iUnion, mem_ball, exists_prop]
    -- The sets `D n i` cover the whole space. Indeed, for each `x` we can choose `n` such that
      -- `ball x (3 / 2 ^ n) ⊆ s (ind x)`, then either `x ∈ D n i`, or `x ∈ D m i` for some `m < n`.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
⊢ ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
[PROOFSTEP]
intro n i y
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
n : ℕ
i : ι
y : α
⊢ y ∈ D n i ↔
    ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
[PROOFSTEP]
rw [Dn n i]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
n : ℕ
i : ι
y : α
⊢ y ∈
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n) ↔
    ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
[PROOFSTEP]
simp only [mem_iUnion, mem_ball, exists_prop]
  -- The sets `D n i` cover the whole space. Indeed, for each `x` we can choose `n` such that
    -- `ball x (3 / 2 ^ n) ⊆ s (ind x)`, then either `x ∈ D n i`, or `x ∈ D m i` for some `m < n`.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have Dcov : ∀ x, ∃ n i, x ∈ D n i := fun x =>
  by
  obtain ⟨n, hn⟩ : ∃ n : ℕ, ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x) := by
    -- This proof takes 5 lines because we can't import `specific_limits` here
    rcases isOpen_iff.1 (ho <| ind x) x (mem_ind x) with ⟨ε, ε0, hε⟩
    have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
    rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩
    refine' ⟨n, Subset.trans (ball_subset_ball _) hε⟩
    simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le
  by_contra' h
  apply h n (ind x)
  exact
    memD.2
      ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_ball_self (pow_pos _)⟩
        -- Each `D n i` is a union of open balls, hence it is an open set
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
⊢ ∃ n i, x ∈ D n i
[PROOFSTEP]
obtain ⟨n, hn⟩ : ∃ n : ℕ, ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x) := by
  -- This proof takes 5 lines because we can't import `specific_limits` here
  rcases isOpen_iff.1 (ho <| ind x) x (mem_ind x) with ⟨ε, ε0, hε⟩
  have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
  rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩
  refine' ⟨n, Subset.trans (ball_subset_ball _) hε⟩
  simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
⊢ ∃ n, ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
[PROOFSTEP]
rcases isOpen_iff.1 (ho <| ind x) x (mem_ind x) with ⟨ε, ε0, hε⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : ball x ε ⊆ s (ind x)
⊢ ∃ n, ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
[PROOFSTEP]
have : 0 < ε / 3 := ENNReal.div_pos_iff.2 ⟨ε0.lt.ne', ENNReal.coe_ne_top⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : ball x ε ⊆ s (ind x)
this : 0 < ε / 3
⊢ ∃ n, ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
[PROOFSTEP]
rcases ENNReal.exists_inv_two_pow_lt this.ne' with ⟨n, hn⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : ball x ε ⊆ s (ind x)
this : 0 < ε / 3
n : ℕ
hn : 2⁻¹ ^ n < ε / 3
⊢ ∃ n, ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
[PROOFSTEP]
refine' ⟨n, Subset.trans (ball_subset_ball _) hε⟩
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
ε : ℝ≥0∞
ε0 : ε > 0
hε : ball x ε ⊆ s (ind x)
this : 0 < ε / 3
n : ℕ
hn : 2⁻¹ ^ n < ε / 3
⊢ 3 * 2⁻¹ ^ n ≤ ε
[PROOFSTEP]
simpa only [div_eq_mul_inv, mul_comm] using (ENNReal.mul_lt_of_lt_div hn).le
[GOAL]
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
n : ℕ
hn : ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
⊢ ∃ n i, x ∈ D n i
[PROOFSTEP]
by_contra' h
[GOAL]
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
n : ℕ
hn : ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
h :
  ∀ (n : ℕ) (i : ι),
    ¬x ∈
        (fun n =>
            Nat.strongRecOn' n fun n D' i =>
              ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ :
                ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j), ball x (2⁻¹ ^ n))
          n i
⊢ False
[PROOFSTEP]
apply h n (ind x)
[GOAL]
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
x : α
n : ℕ
hn : ball x (3 * 2⁻¹ ^ n) ⊆ s (ind x)
h :
  ∀ (n : ℕ) (i : ι),
    ¬x ∈
        (fun n =>
            Nat.strongRecOn' n fun n D' i =>
              ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ :
                ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j), ball x (2⁻¹ ^ n))
          n i
⊢ x ∈
    (fun n =>
        Nat.strongRecOn' n fun n D' i =>
          ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
            ball x (2⁻¹ ^ n))
      n (ind x)
[PROOFSTEP]
exact
  memD.2
    ⟨x, rfl, hn, fun _ _ _ => h _ _, mem_ball_self (pow_pos _)⟩
      -- Each `D n i` is a union of open balls, hence it is an open set
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have Dopen : ∀ n i, IsOpen (D n i) := fun n i => by
  rw [Dn]
  iterate 4 refine' isOpen_iUnion fun _ => _
  exact isOpen_ball
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
⊢ IsOpen (D n i)
[PROOFSTEP]
rw [Dn]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
⊢ IsOpen
    (⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
      ball x (2⁻¹ ^ n))
[PROOFSTEP]
iterate 4 refine' isOpen_iUnion fun _ => _
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
⊢ IsOpen
    (⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
      ball x (2⁻¹ ^ n))
[PROOFSTEP]
refine' isOpen_iUnion fun _ => _
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝¹ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
x✝ : α
⊢ IsOpen
    (⋃ (_ : ind x✝ = i) (_ : ball x✝ (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x✝ ∈ D m j),
      ball x✝ (2⁻¹ ^ n))
[PROOFSTEP]
refine' isOpen_iUnion fun _ => _
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝² : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
x✝¹ : α
x✝ : ind x✝¹ = i
⊢ IsOpen (⋃ (_ : ball x✝¹ (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x✝¹ ∈ D m j), ball x✝¹ (2⁻¹ ^ n))
[PROOFSTEP]
refine' isOpen_iUnion fun _ => _
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝³ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
x✝² : α
x✝¹ : ind x✝² = i
x✝ : ball x✝² (3 * 2⁻¹ ^ n) ⊆ s i
⊢ IsOpen (⋃ (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x✝² ∈ D m j), ball x✝² (2⁻¹ ^ n))
[PROOFSTEP]
refine' isOpen_iUnion fun _ => _
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝⁴ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
n : ℕ
i : ι
x✝³ : α
x✝² : ind x✝³ = i
x✝¹ : ball x✝³ (3 * 2⁻¹ ^ n) ⊆ s i
x✝ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x✝³ ∈ D m j
⊢ IsOpen (ball x✝³ (2⁻¹ ^ n))
[PROOFSTEP]
exact isOpen_ball
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
have HDS : ∀ n i, D n i ⊆ s i := fun n i x => by
  rw [memD]
  rintro ⟨y, rfl, hsub, -, hyx⟩
  refine hsub (hyx.trans_le <| le_mul_of_one_le_left' ?_)
  norm_num1
    -- Let us show the rest of the properties. Since the definition expects a family indexed
      -- by a single parameter, we use `ℕ × ι` as the domain.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
n : ℕ
i : ι
x : α
⊢ x ∈ D n i → x ∈ s i
[PROOFSTEP]
rw [memD]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
n : ℕ
i : ι
x : α
⊢ (∃ x_1,
      ind x_1 = i ∧
        ball x_1 (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x_1 ∈ D m j) ∧ edist x x_1 < 2⁻¹ ^ n) →
    x ∈ s i
[PROOFSTEP]
rintro ⟨y, rfl, hsub, -, hyx⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
n : ℕ
x y : α
hsub : ball y (3 * 2⁻¹ ^ n) ⊆ s (ind y)
hyx : edist x y < 2⁻¹ ^ n
⊢ x ∈ s (ind y)
[PROOFSTEP]
refine hsub (hyx.trans_le <| le_mul_of_one_le_left' ?_)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
n : ℕ
x y : α
hsub : ball y (3 * 2⁻¹ ^ n) ⊆ s (ind y)
hyx : edist x y < 2⁻¹ ^ n
⊢ 1 ≤ 3
[PROOFSTEP]
norm_num1
  -- Let us show the rest of the properties. Since the definition expects a family indexed
    -- by a single parameter, we use `ℕ × ι` as the domain.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
⊢ ∃ β t x x, LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
[PROOFSTEP]
refine'
  ⟨ℕ × ι, fun ni => D ni.1 ni.2, fun _ => Dopen _ _, _, _, fun ni => ⟨ni.2, HDS _ _⟩⟩
    -- The sets `D n i` cover the whole space as we proved earlier
[GOAL]
case refine'_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
⊢ ⋃ (b : ℕ × ι), (fun ni => D ni.fst ni.snd) b = univ
[PROOFSTEP]
refine' iUnion_eq_univ_iff.2 fun x => _
[GOAL]
case refine'_1
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
⊢ ∃ i, x ∈ (fun ni => D ni.fst ni.snd) i
[PROOFSTEP]
rcases Dcov x with ⟨n, i, h⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
h : x ∈ D n i
⊢ ∃ i, x ∈ (fun ni => D ni.fst ni.snd) i
[PROOFSTEP]
exact
  ⟨⟨n, i⟩, h⟩
    /- Let us prove that the covering `D n i` is locally finite. Take a point `x` and choose
        `n`, `i` so that `x ∈ D n i`. Since `D n i` is an open set, we can choose `k` so that
        `B = ball x (1 / 2 ^ (n + k + 1)) ⊆ D n i`. -/
[GOAL]
case refine'_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
⊢ LocallyFinite fun ni => D ni.fst ni.snd
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ t)}
[PROOFSTEP]
rcases Dcov x with ⟨n, i, hn⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ t)}
[PROOFSTEP]
have : D n i ∈ 𝓝 x := IsOpen.mem_nhds (Dopen _ _) hn
[GOAL]
case refine'_2.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ t)}
[PROOFSTEP]
rcases(nhds_basis_uniformity uniformity_basis_edist_inv_two_pow).mem_iff.1 this with
  ⟨k, -, hsub : ball x (2⁻¹ ^ k) ⊆ D n i⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ t)}
[PROOFSTEP]
set B := ball x (2⁻¹ ^ (n + k + 1))
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
⊢ ∃ t, t ∈ 𝓝 x ∧ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ t)}
[PROOFSTEP]
refine'
  ⟨B, ball_mem_nhds _ (pow_pos _), _⟩
    -- The sets `D m i`, `m > n + k`, are disjoint with `B`
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
⊢ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
[PROOFSTEP]
have Hgt : ∀ m ≥ n + k + 1, ∀ (i : ι), Disjoint (D m i) B := fun m hm i =>
  by
  rw [disjoint_iff_inf_le]
  rintro y ⟨hym, hyx⟩
  rcases memD.1 hym with ⟨z, rfl, _hzi, H, hz⟩
  have : z ∉ ball x (2⁻¹ ^ k) := fun hz' => H n (by linarith) i (hsub hz')
  apply this
  calc
    edist z x ≤ edist y z + edist y x := edist_triangle_left _ _ _
    _ < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) := (ENNReal.add_lt_add hz hyx)
    _ ≤ 2⁻¹ ^ (k + 1) + 2⁻¹ ^ (k + 1) := (add_le_add (hpow_le <| by linarith) (hpow_le <| by linarith))
    _ = 2⁻¹ ^ k := by
      rw [← two_mul, h2pow]
        -- For each `m ≤ n + k` there is at most one `j` such that `D m j ∩ B` is nonempty.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i✝ : ι
hn : x ∈ D n i✝
this : D n i✝ ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i✝
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
i : ι
⊢ Disjoint (D m i) B
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i✝ : ι
hn : x ∈ D n i✝
this : D n i✝ ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i✝
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
i : ι
⊢ D m i ⊓ B ≤ ⊥
[PROOFSTEP]
rintro y ⟨hym, hyx⟩
[GOAL]
case intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i✝ : ι
hn : x ∈ D n i✝
this : D n i✝ ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i✝
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
i : ι
y : α
hym : y ∈ D m i
hyx : y ∈ B
⊢ y ∈ ⊥
[PROOFSTEP]
rcases memD.1 hym with ⟨z, rfl, _hzi, H, hz⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
⊢ y ∈ ⊥
[PROOFSTEP]
have : z ∉ ball x (2⁻¹ ^ k) := fun hz' => H n (by linarith) i (hsub hz')
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
hz' : z ∈ ball x (2⁻¹ ^ k)
⊢ n < m
[PROOFSTEP]
linarith
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
this : ¬z ∈ ball x (2⁻¹ ^ k)
⊢ y ∈ ⊥
[PROOFSTEP]
apply this
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
this : ¬z ∈ ball x (2⁻¹ ^ k)
⊢ z ∈ ball x (2⁻¹ ^ k)
[PROOFSTEP]
calc
  edist z x ≤ edist y z + edist y x := edist_triangle_left _ _ _
  _ < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) := (ENNReal.add_lt_add hz hyx)
  _ ≤ 2⁻¹ ^ (k + 1) + 2⁻¹ ^ (k + 1) := (add_le_add (hpow_le <| by linarith) (hpow_le <| by linarith))
  _ = 2⁻¹ ^ k := by
    rw [← two_mul, h2pow]
      -- For each `m ≤ n + k` there is at most one `j` such that `D m j ∩ B` is nonempty.
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
this : ¬z ∈ ball x (2⁻¹ ^ k)
⊢ k + 1 ≤ m
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
this : ¬z ∈ ball x (2⁻¹ ^ k)
⊢ k + 1 ≤ n + k + 1
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
m : ℕ
hm : m ≥ n + k + 1
y : α
hyx : y ∈ B
z : α
hym : y ∈ D m (ind z)
_hzi : ball z (3 * 2⁻¹ ^ m) ⊆ s (ind z)
H : ∀ (m_1 : ℕ), m_1 < m → ∀ (j : ι), ¬z ∈ D m_1 j
hz : edist y z < 2⁻¹ ^ m
this : ¬z ∈ ball x (2⁻¹ ^ k)
⊢ 2⁻¹ ^ (k + 1) + 2⁻¹ ^ (k + 1) = 2⁻¹ ^ k
[PROOFSTEP]
rw [← two_mul, h2pow]
  -- For each `m ≤ n + k` there is at most one `j` such that `D m j ∩ B` is nonempty.
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
⊢ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
[PROOFSTEP]
have Hle : ∀ m ≤ n + k, Set.Subsingleton {j | (D m j ∩ B).Nonempty} :=
  by
  rintro m hm j₁ ⟨y, hyD, hyB⟩ j₂ ⟨z, hzD, hzB⟩
  by_contra' h' : j₁ ≠ j₂
  wlog h : j₁ < j₂ generalizing j₁ j₂ y z
  · exact this z hzD hzB y hyD hyB h'.symm (h'.lt_or_lt.resolve_left h)
  rcases memD.1 hyD with ⟨y', rfl, hsuby, -, hdisty⟩
  rcases memD.1 hzD with ⟨z', rfl, -, -, hdistz⟩
  suffices : edist z' y' < 3 * 2⁻¹ ^ m
  exact nmem_of_lt_ind h (hsuby this)
  calc
    edist z' y' ≤ edist z' x + edist x y' := edist_triangle _ _ _
    _ ≤ edist z z' + edist z x + (edist y x + edist y y') :=
      (add_le_add (edist_triangle_left _ _ _) (edist_triangle_left _ _ _))
    _ < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) + (2⁻¹ ^ (n + k + 1) + 2⁻¹ ^ m) := by apply_rules [ENNReal.add_lt_add]
    _ = 2 * (2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1)) := by simp only [two_mul, add_comm]
    _ ≤ 2 * (2⁻¹ ^ m + 2⁻¹ ^ (m + 1)) := by gcongr 2 * (_ + ?_); exact hpow_le (add_le_add hm le_rfl)
    _ = 3 * 2⁻¹ ^ m := by
      rw [mul_add, h2pow, ← two_add_one_eq_three, add_mul, one_mul]
        -- Finally, we glue `Hgt` and `Hle`
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
⊢ ∀ (m : ℕ), m ≤ n + k → Set.Subsingleton {j | Set.Nonempty (D m j ∩ B)}
[PROOFSTEP]
rintro m hm j₁ ⟨y, hyD, hyB⟩ j₂ ⟨z, hzD, hzB⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
j₁ : ι
y : α
hyD : y ∈ D m j₁
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
⊢ j₁ = j₂
[PROOFSTEP]
by_contra' h' : j₁ ≠ j₂
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
j₁ : ι
y : α
hyD : y ∈ D m j₁
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
h' : j₁ ≠ j₂
⊢ False
[PROOFSTEP]
wlog h : j₁ < j₂ generalizing j₁ j₂ y z
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
j₁ : ι
y : α
hyD : y ∈ D m j₁
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
h' : j₁ ≠ j₂
this : ∀ ⦃j₁ : ι⦄ (y : α), y ∈ D m j₁ → y ∈ B → ∀ ⦃j₂ : ι⦄ (z : α), z ∈ D m j₂ → z ∈ B → j₁ ≠ j₂ → j₁ < j₂ → False
h : ¬j₁ < j₂
⊢ False
[PROOFSTEP]
exact this z hzD hzB y hyD hyB h'.symm (h'.lt_or_lt.resolve_left h)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
j₁ : ι
y : α
hyD : y ∈ D m j₁
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
h' : j₁ ≠ j₂
h : j₁ < j₂
⊢ False
[PROOFSTEP]
rcases memD.1 hyD with ⟨y', rfl, hsuby, -, hdisty⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
j₂ : ι
z : α
hzD : z ∈ D m j₂
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
h' : ind y' ≠ j₂
h : ind y' < j₂
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
⊢ False
[PROOFSTEP]
rcases memD.1 hzD with ⟨z', rfl, -, -, hdistz⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ False
[PROOFSTEP]
suffices : edist z' y' < 3 * 2⁻¹ ^ m
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
this : edist z' y' < 3 * 2⁻¹ ^ m
⊢ False
case this
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ edist z' y' < 3 * 2⁻¹ ^ m
[PROOFSTEP]
exact nmem_of_lt_ind h (hsuby this)
[GOAL]
case this
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ edist z' y' < 3 * 2⁻¹ ^ m
[PROOFSTEP]
calc
  edist z' y' ≤ edist z' x + edist x y' := edist_triangle _ _ _
  _ ≤ edist z z' + edist z x + (edist y x + edist y y') :=
    (add_le_add (edist_triangle_left _ _ _) (edist_triangle_left _ _ _))
  _ < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) + (2⁻¹ ^ (n + k + 1) + 2⁻¹ ^ m) := by apply_rules [ENNReal.add_lt_add]
  _ = 2 * (2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1)) := by simp only [two_mul, add_comm]
  _ ≤ 2 * (2⁻¹ ^ m + 2⁻¹ ^ (m + 1)) := by gcongr 2 * (_ + ?_); exact hpow_le (add_le_add hm le_rfl)
  _ = 3 * 2⁻¹ ^ m := by
    rw [mul_add, h2pow, ← two_add_one_eq_three, add_mul, one_mul]
      -- Finally, we glue `Hgt` and `Hle`
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ edist z z' + edist z x + (edist y x + edist y y') < 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) + (2⁻¹ ^ (n + k + 1) + 2⁻¹ ^ m)
[PROOFSTEP]
apply_rules [ENNReal.add_lt_add]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ 2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1) + (2⁻¹ ^ (n + k + 1) + 2⁻¹ ^ m) = 2 * (2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1))
[PROOFSTEP]
simp only [two_mul, add_comm]
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ 2 * (2⁻¹ ^ m + 2⁻¹ ^ (n + k + 1)) ≤ 2 * (2⁻¹ ^ m + 2⁻¹ ^ (m + 1))
[PROOFSTEP]
gcongr 2 * (_ + ?_)
[GOAL]
case bc.bc
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ 2⁻¹ ^ (n + k + 1) ≤ 2⁻¹ ^ (m + 1)
[PROOFSTEP]
exact hpow_le (add_le_add hm le_rfl)
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
m : ℕ
hm : m ≤ n + k
y : α
hyB : y ∈ B
z : α
hzB : z ∈ B
y' : α
hyD : y ∈ D m (ind y')
hsuby : ball y' (3 * 2⁻¹ ^ m) ⊆ s (ind y')
hdisty : edist y y' < 2⁻¹ ^ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < 2⁻¹ ^ m
⊢ 2 * (2⁻¹ ^ m + 2⁻¹ ^ (m + 1)) = 3 * 2⁻¹ ^ m
[PROOFSTEP]
rw [mul_add, h2pow, ← two_add_one_eq_three, add_mul, one_mul]
  -- Finally, we glue `Hgt` and `Hle`
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ), m ≤ n + k → Set.Subsingleton {j | Set.Nonempty (D m j ∩ B)}
⊢ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
[PROOFSTEP]
have : (⋃ (m ≤ n + k) (i ∈ {i : ι | (D m i ∩ B).Nonempty}), {(m, i)}).Finite :=
  (finite_le_nat _).biUnion' fun i hi => (Hle i hi).finite.biUnion' fun _ _ => finite_singleton _
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ), m ≤ n + k → Set.Subsingleton {j | Set.Nonempty (D m j ∩ B)}
this : Set.Finite (⋃ (m : ℕ) (_ : m ≤ n + k) (i : ι) (_ : i ∈ {i | Set.Nonempty (D m i ∩ B)}), {(m, i)})
⊢ Set.Finite {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
[PROOFSTEP]
refine' this.subset fun I hI => _
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ), m ≤ n + k → Set.Subsingleton {j | Set.Nonempty (D m j ∩ B)}
this : Set.Finite (⋃ (m : ℕ) (_ : m ≤ n + k) (i : ι) (_ : i ∈ {i | Set.Nonempty (D m i ∩ B)}), {(m, i)})
I : ℕ × ι
hI : I ∈ {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
⊢ I ∈ ⋃ (m : ℕ) (_ : m ≤ n + k) (i : ι) (_ : i ∈ {i | Set.Nonempty (D m i ∩ B)}), {(m, i)}
[PROOFSTEP]
simp only [mem_iUnion]
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ), m ≤ n + k → Set.Subsingleton {j | Set.Nonempty (D m j ∩ B)}
this : Set.Finite (⋃ (m : ℕ) (_ : m ≤ n + k) (i : ι) (_ : i ∈ {i | Set.Nonempty (D m i ∩ B)}), {(m, i)})
I : ℕ × ι
hI : I ∈ {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
⊢ ∃ i h i_1 i_2, I ∈ {(i, i_1)}
[PROOFSTEP]
refine' ⟨I.1, _, I.2, hI, Prod.mk.eta.symm⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
inst✝ : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < 2⁻¹ ^ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → 2⁻¹ ^ n ≤ 2⁻¹ ^ m
h2pow : ∀ (n : ℕ), 2 * 2⁻¹ ^ (n + 1) = 2⁻¹ ^ n
ι : Type u_1
s : ι → Set α
ho : ∀ (a : ι), IsOpen (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
x✝ : LinearOrder ι := linearOrderOfSTO WellOrderingRel
wf : WellFounded fun x x_1 => x < x_1
ind : α → ι := fun x => WellFounded.min wf {i | x ∈ s i} (_ : ∃ i, x ∈ s i)
mem_ind : ∀ (x : α), x ∈ s (ind x)
nmem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → ¬x ∈ s i
D : ℕ → ι → Set α :=
  fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
hD :
  D = fun n =>
    Nat.strongRecOn' n fun n D' i =>
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ) (H : m < n) (j : ι), ¬x ∈ D' m H j),
        ball x (2⁻¹ ^ n)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α) (_ : ind x = i) (_ : ball x (3 * 2⁻¹ ^ n) ⊆ s i) (_ : ∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j),
        ball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ x, ind x = i ∧ ball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ (m : ℕ), m < n → ∀ (j : ι), ¬x ∈ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen (D n i)
HDS : ∀ (n : ℕ) (i : ι), D n i ⊆ s i
x : α
n : ℕ
i : ι
hn : x ∈ D n i
this✝ : D n i ∈ 𝓝 x
k : ℕ
hsub : ball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := ball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), m ≥ n + k + 1 → ∀ (i : ι), Disjoint (D m i) B
Hle : ∀ (m : ℕ), m ≤ n + k → Set.Subsingleton {j | Set.Nonempty (D m j ∩ B)}
this : Set.Finite (⋃ (m : ℕ) (_ : m ≤ n + k) (i : ι) (_ : i ∈ {i | Set.Nonempty (D m i ∩ B)}), {(m, i)})
I : ℕ × ι
hI : I ∈ {i | Set.Nonempty ((fun ni => D ni.fst ni.snd) i ∩ B)}
⊢ I.fst ≤ n + k
[PROOFSTEP]
exact not_lt.1 fun hlt => (Hgt I.1 hlt I.2).le_bot hI.choose_spec