-- Lean 4 proof step from Mathlib.MeasureTheory.Covering.Besicovitch (goal)
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : SecondCountableTopology α
inst_2 : MeasurableSpace α
inst_3 : OpensMeasurableSpace α
μ : Measure α
inst_4 : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty.{u_1 + 1} (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) o : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a : BallPackage (↑s : Type u_1) α :=
  { c := fun (x : (↑s : Type u_1)) ↦ (↑x : α), r := fun (x : (↑s : Type u_1)) ↦ r (↑x : α), rpos := ⋯, r_bound := 1,
    r_le := ⋯ }
u : Fin N → Set (↑s : Type u_1)
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint (α := Set α) fun (j : (↑s : Type u_1)) ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun (i : Fin N) ↦ ⋃ x ∈ u i, closedBall (↑x : α) (r (↑x : α))
A : s = ⋃ (i : Fin N), s ∩ v i
S :
  LE.le (α := ℝ≥0∞)
    (∑ _i : Fin N, HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑N : ℝ≥0∞) : ℝ≥0∞))
    (∑ i : Fin N, (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i))
i : Fin N
hi :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ v i)
B :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (o ∩ v i) : ℝ≥0∞)
    (∑' (x : (↑(u i) : Type u_1)),
        (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) :
      ℝ≥0∞)
w : Finset (↑(u i) : Type u_1)
hw :
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) <
    ∑ x ∈ w, (μ : (a : Set α) → ℝ≥0∞) (o ∩ closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α)))
μ₁ :
  (μ : (a : Set α) → ℝ≥0∞) o =
    HMul.hMul (β := ℝ≥0∞) (1 / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
      HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) o ≤
    HAdd.hAdd (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o) :
        ℝ≥0∞)
      (HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
have μ₂ : HMul.hMul (β := ℝ≥0∞) (1 / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) +
    HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        ((⋃ x ∈ w, closedBall (↑(↑x : (↑s : Type u_1)) : α) (r (↑(↑x : (↑s : Type u_1)) : α))) ∩ o) :
      ℝ≥0∞)
    (HMul.hMul (β := ℝ≥0∞) ((↑N : ℝ≥0∞) / HAdd.hAdd (α := ℝ≥0∞) (↑N : ℝ≥0∞) 1) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
Tactic: calc
      μ o = 1 / (N + 1) * μ s + N / (N + 1) * μ s := by
        rw [μo, ← add_mul, ENNReal.div_add_div_same, add_comm, ENNReal.div_self, one_mul] <;> simp
      _ ≤ μ ((⋃ x ∈ w, closedBall (↑x) (r ↑x)) ∩ o) + N / (N + 1) * μ s := by
        gcongr
        rw [one_div, mul_comm, ← div_eq_mul_inv]
        apply hw.le.trans (le_of_eq _)
        rw [← Finset.set_biUnion_coe, inter_comm _ o, inter_iUnion₂, Finset.set_biUnion_coe,
          measure_biUnion_finset]
        · have : (w : Set (u i)).PairwiseDisjoint
              fun b : u i => closedBall (b : α) (r (b : α)) := by
            intro k _ l _ hkl; exact hu i k.2 l.2 (Subtype.val_injective.ne hkl)
          exact this.mono fun k => inter_subset_right
        · intro b _
          apply omeas.inter measurableSet_closedBall