-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Paracompact (goal)
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 : ι
⊢ 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 α)
have 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))
Tactic: rw [Nat.strongRecOn'_beta]