no goals
α : Type u_1
inst✝¹ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : FineSubfamilyOn v f s
inst✝ : SecondCountableTopology α
ρ : MeasureTheory.Measure α
hρ : ρ ≪ μ
⊢ s ⊆
    (s \ ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) ∪
      ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p
simp only [subset_union_left, diff_union_self]
no goals
α : Type u_1
inst✝¹ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : FineSubfamilyOn v f s
inst✝ : SecondCountableTopology α
ρ : MeasureTheory.Measure α
hρ : ρ ≪ μ
⊢ ↑↑ρ (s \ ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) +
      ↑↑ρ (⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) =
    ∑' (p : ↑(FineSubfamilyOn.index h)), ↑↑ρ (FineSubfamilyOn.covering h ↑p)
rw [hρ h.measure_diff_biUnion, zero_add,
  measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]