-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.LiminfLimsup (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
μ : Measure α
inst_4 : IsLocallyFiniteMeasure μ
inst_5 : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun (i : ℕ) ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun (i : ℕ) ↦ ⋃ (j : ℕ), ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) W : ℝ≥0∞) (0 : ℝ≥0∞)
d : α
hd' :
  ∀ {ι : Type} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (β := ℝ≥0∞)
          (fun (j : ι) ↦
            HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (W ∩ closedBall (w j) (δ j)) : ℝ≥0∞)
              ((μ : (a : Set α) → ℝ≥0∞) (closedBall (w j) (δ j)) : ℝ≥0∞))
          l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : (j : ℕ) → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
hC : C ≠ 0
b : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (M * r₁ (f j))
B : ℕ → Set α := fun (j : ℕ) ↦ closedBall (w j) (r₁ (f j))
h₁ : ∀ (j : ℕ), b j ⊆ B j
h₂ : ∀ (j : ℕ), W ∩ B j ⊆ B j
h₃ : ∀ᶠ (j : ℕ) in atTop, Disjoint (b j) (W ∩ B j)
h₄ :
  ∀ᶠ (j : ℕ) in atTop,
    (μ : (a : Set α) → ℝ≥0∞) (B j) ≤ HMul.hMul (β := ℝ≥0∞) (↑C : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (b j) : ℝ≥0∞)
j : ℕ
hB : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≠ ∞
hj₁ : Disjoint (b j) (W ∩ B j)
hj₂ : HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤ (μ : (a : Set α) → ℝ≥0∞) (b j)
hj₃ :
  HAdd.hAdd (β := ℝ≥0∞) (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
        ((μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) : ℝ≥0∞) -
      HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
⊢ (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
have inr : ∀
  (hj₃ :
    (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
      HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
        (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))),
  (μ : (a : Set α) → ℝ≥0∞) (W ∩ B j) ≤
    HSub.hSub (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) (↑C⁻¹ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (B j) : ℝ≥0∞))
Tactic: rwa [ENNReal.add_sub_cancel_left hB] at hj₃
Cleared hypotheses: hj₃