-- Module: Mathlib.Topology.EMetricSpace.Paracompact
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pow_pos : ∀ (k : ℕ), 0 < HPow.hPow (α := ℝ≥0∞) 2⁻¹ k
hpow_le : ∀ {m n : ℕ}, m ≤ n → HPow.hPow (α := ℝ≥0∞) 2⁻¹ n ≤ HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
h2pow : ∀ (n : ℕ), 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + 1) = HPow.hPow (α := ℝ≥0∞) 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 : (x : α) → ι := fun (x : α) ↦ WellFounded.min (r := fun (x1 x2 : ι) ↦ x1 < x2) ⋯ {i : ι | x ∈ s i} ⋯
mem_ind : ∀ (x : α), x ∈ s (ind x)
notMem_of_lt_ind : ∀ {x : α} {i : ι} (hlt : i < ind x) (hxi : x ∈ s i), False
D : ℕ → ι → Set α :=
  fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
hD :
  D = fun (n : ℕ) ↦
    n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α) fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
n : ℕ
i : ι
rw rw₁ :
  Eq.{u_1 + 1} (α := Set α)
    (⋃ (x : α),
      ⋃ (_ : ind x = i),
        ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
          ⋃ (_ :
            ∀ (m : ℕ) (H : m < n) (j : ι),
              x ∉
                (fun (m : ℕ) (x : m < n) ↦
                    (m.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α)
                        fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
                        ⋃ (x : α),
                          ⋃ (_ : ind x = i),
                            ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
                              ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j),
                                eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) :
                      ι → Set α))
                  m H j),
            eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n))
    (⋃ (x : α),
      ⋃ (_ : ind x = i),
        ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
          ⋃ (_ :
            ∀ m < n,
              ∀ (j : ι),
                x ∉
                  (m.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α)
                      (fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
                        ⋃ (x : α),
                          ⋃ (_ : ind x = i),
                            ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
                              ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j),
                                eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n))
                      j :
                    Set α)),
            eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n))
⊢ Eq.{u_1 + 1} (α := Set α)
    (n.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α)
        (fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
          ⋃ (x : α),
            ⋃ (_ : ind x = i),
              ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
                ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n))
        i :
      Set α)
    (⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ :
              ∀ m < n,
                ∀ (j : ι),
                  x ∉
                    (m.strongRecOn' (P := fun (x : ℕ) ↦ ι → Set α)
                        (fun (n : ℕ) (D' : (m : ℕ) → m < n → ι → Set α) (i : ι) ↦
                          ⋃ (x : α),
                            ⋃ (_ : ind x = i),
                              ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
                                ⋃ (_ : ∀ (m : ℕ) (H : m < n) (j : ι), x ∉ D' m H j),
                                  eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n))
                        j :
                      Set α)),
              eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) :
      Set α)

Tactic:
rw [Nat.strongRecOn'_beta]

Premises used: Nat.strongRecOn'_beta