-- 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)
Dn :
  ∀ (n : ℕ) (i : ι),
    D n i =
      ⋃ (x : α),
        ⋃ (_ : ind x = i),
          ⋃ (_ : eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i),
            ⋃ (_ : ∀ m < n, ∀ (j : ι), x ∉ D m j), eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ n)
memD :
  ∀ {n : ℕ} {i : ι} {y : α},
    y ∈ D n i ↔
      ∃ (x : α),
        ind x = i ∧
          eball x (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ n) ⊆ s i ∧
            (∀ m < n, ∀ (j : ι), x ∉ D m j) ∧ edist y x < HPow.hPow (α := ℝ≥0∞) 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 (HPow.hPow (α := ℝ≥0∞) 2⁻¹ k) ⊆ D n i
B : Set α := eball x (HPow.hPow (α := ℝ≥0∞) 2⁻¹ (n + k + 1))
Hgt : ∀ (m : ℕ) (hm : n + k + 1 ≤ m) (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 : eball y' (3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m) ⊆ s (ind y')
hdisty : edist y y' < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
z' : α
hzD : z ∈ D m (ind z')
h' : ind y' ≠ ind z'
h : ind y' < ind z'
hdistz : edist z z' < HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
rw : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m + 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ (m + 1) = 3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
rw₁ : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m + HPow.hPow (α := ℝ≥0∞) 2⁻¹ m = 3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
rw₂ :
  2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m + HPow.hPow (α := ℝ≥0∞) 2⁻¹ m =
    HAdd.hAdd (α := ℝ≥0∞) 2 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
⊢ 2 * (HPow.hPow (α := ℝ≥0∞) 2⁻¹ m + HPow.hPow (α := ℝ≥0∞) 2⁻¹ (m + 1)) = 3 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
have rw₃ : 2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m + HPow.hPow (α := ℝ≥0∞) 2⁻¹ m =
  2 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m + 1 * HPow.hPow (α := ℝ≥0∞) 2⁻¹ m
Tactic: rw [mul_add, h2pow, ← two_add_one_eq_three, add_mul, one_mul]