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
⊢ LocallyFinite fun ni ↦ D ni.1 ni.2

Tactic:
· intro x
    rcases Dcov x with ⟨n, i, hn⟩
    have : D n i ∈ 𝓝 x := IsOpen.mem_nhds (Dopen _ _) hn
    rcases (nhds_basis_uniformity uniformity_basis_edist_inv_two_pow).mem_iff.1 this with
      ⟨k, -, hsub : eball x (2⁻¹ ^ k) ⊆ D n i⟩
    set B := eball x (2⁻¹ ^ (n + k + 1))
    refine ⟨B, eball_mem_nhds _ (pow_pos _), ?_⟩
    -- The sets `D m i`, `m > n + k`, are disjoint with `B`
    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]
    -- For each `m ≤ n + k` there is at most one `j` such that `D m j ∩ B` is nonempty.
    have Hle (m) (hm : m ≤ n + k) : Set.Subsingleton { j | (D m j ∩ B).Nonempty } := by
      rintro 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_gt.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 from notMem_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`
    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 _
    refine this.subset fun I hI => ?_
    simp only [mem_iUnion]
    refine ⟨I.1, ?_, I.2, hI, rfl⟩
    exact not_lt.1 fun hlt => (Hgt I.1 hlt I.2).le_bot hI.choose_spec

Goal state after: