case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ (x : α), x ∈ s → ∀ (δ : ℝ), δ > 0 → Set.Nonempty (f x ∩ Ioo 0 δ)
ν : MeasureTheory.Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ ∃ t,
    Set.Countable t ∧
      (∀ (p : α × ℝ), p ∈ t → p.fst ∈ s) ∧
        (∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst) ∧
          ↑↑μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0 ∧
            PairwiseDisjoint t fun p => closedBall p.fst p.snd
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ (x : α), x ∈ s → ∀ (δ : ℝ), δ > 0 → Set.Nonempty (f x ∩ Ioo 0 δ)
⊢ ∃ t,
    Set.Countable t ∧
      (∀ (p : α × ℝ), p ∈ t → p.fst ∈ s) ∧
        (∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst) ∧
          ↑↑μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0 ∧
            PairwiseDisjoint t fun p => closedBall p.fst p.snd
rcases exists_absolutelyContinuous_isFiniteMeasure μ with ⟨ν, hν, hμν⟩
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ (x : α), x ∈ s → ∀ (δ : ℝ), δ > 0 → Set.Nonempty (f x ∩ Ioo 0 δ)
ν : MeasureTheory.Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
t : Set (α × ℝ)
t_count : Set.Countable t
ts : ∀ (p : α × ℝ), p ∈ t → p.fst ∈ s
tr : ∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst
tν : ↑↑ν (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0
tdisj : PairwiseDisjoint t fun p => closedBall p.fst p.snd
⊢ ∃ t,
    Set.Countable t ∧
      (∀ (p : α × ℝ), p ∈ t → p.fst ∈ s) ∧
        (∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst) ∧
          ↑↑μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0 ∧
            PairwiseDisjoint t fun p => closedBall p.fst p.snd
case intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ (x : α), x ∈ s → ∀ (δ : ℝ), δ > 0 → Set.Nonempty (f x ∩ Ioo 0 δ)
ν : MeasureTheory.Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ ∃ t,
    Set.Countable t ∧
      (∀ (p : α × ℝ), p ∈ t → p.fst ∈ s) ∧
        (∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst) ∧
          ↑↑μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0 ∧
            PairwiseDisjoint t fun p => closedBall p.fst p.snd
rcases exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux ν f s hf with
  ⟨t, t_count, ts, tr, tν, tdisj⟩
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝⁵ : MetricSpace α
β : Type u
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : MeasureTheory.Measure α
inst✝ : SigmaFinite μ
f : α → Set ℝ
s : Set α
hf : ∀ (x : α), x ∈ s → ∀ (δ : ℝ), δ > 0 → Set.Nonempty (f x ∩ Ioo 0 δ)
ν : MeasureTheory.Measure α
hν : IsFiniteMeasure ν
hμν : μ ≪ ν
t : Set (α × ℝ)
t_count : Set.Countable t
ts : ∀ (p : α × ℝ), p ∈ t → p.fst ∈ s
tr : ∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst
tν : ↑↑ν (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0
tdisj : PairwiseDisjoint t fun p => closedBall p.fst p.snd
⊢ ∃ t,
    Set.Countable t ∧
      (∀ (p : α × ℝ), p ∈ t → p.fst ∈ s) ∧
        (∀ (p : α × ℝ), p ∈ t → p.snd ∈ f p.fst) ∧
          ↑↑μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.fst p.snd) = 0 ∧
            PairwiseDisjoint t fun p => closedBall p.fst p.snd
exact ⟨t, t_count, ts, tr, hμν tν, tdisj⟩