Module: Mathlib.Topology.EMetricSpace.Paracompact

Goal state before:
pp: 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[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (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 : eball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := eball x (2⁻¹ ^ (n + k + 1))
⊢ {i | ((fun ni ↦ D ni.1 ni.2) i ∩ B).Nonempty}.Finite

Tactic:
have Hgt (m) (hm : n + k + 1 ≤ m) (i : ι) : Disjoint (D m i) B := by
      rw [disjoint_iff_inf_le]
      rintro y ⟨hym, hyx⟩
      rcases memD.1 hym with ⟨z, rfl, _hzi, H, hz⟩
      have : z ∉ eball x (2⁻¹ ^ k) := fun hz' => H n (by lia) 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 lia) (hpow_le <| by lia))
        _ = 2⁻¹ ^ k := by rw [← two_mul, h2pow]

Goal state after:
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[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (s a)
hcov : ∀ (x : α), ∃ i, x ∈ s i
w✝ : LinearOrder ι
wf : WellFoundedLT ι
ind : α → ι := fun x ↦ ⋯.min {i | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι}, i < ind x → x ∈ s i → False
D : ℕ → ι → Set α :=
  fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
hD :
  D = fun t ↦
    Nat.strongRec (motive := fun x ↦ ι → Set α)
      (fun n D' i ↦
        ⋃ x,
          ⋃ (_ : ind x = i),
            ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (2⁻¹ ^ n))
      t
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ x,
        ⋃ (_ : ind x = i), ⋃ (_ : eball x (3 * 2⁻¹ ^ n) ⊆ s i), ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (2⁻¹ ^ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔ ∃ x, ind x = i ∧ eball x (3 * 2⁻¹ ^ n) ⊆ s i ∧ (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < 2⁻¹ ^ n
Dcov : ∀ (x : α), ∃ n i, x ∈ D n i
Dopen : ∀ (n : ℕ) (i : ι), IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (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 : eball x (2⁻¹ ^ k) ⊆ D n i
B : Set α := eball x (2⁻¹ ^ (n + k + 1))
Hgt : ∀ (m : ℕ), n + k + 1 ≤ m → ∀ (i : ι), Disjoint (D m i) B
⊢ {i | ((fun ni ↦ D ni.1 ni.2) i ∩ B).Nonempty}.Finite