[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ν : Measure α
hν : ν ≪ μ
s : Set α
f : α → Set (Set α)
h : ∀ (x : α), x ∈ s → f x ⊆ setsAt v x
h' : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑ν (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
rcases v.covering s f h h' with ⟨t, ts, disj, mem_f, hμ⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ν : Measure α
hν : ν ≪ μ
s : Set α
f : α → Set (Set α)
h : ∀ (x : α), x ∈ s → f x ⊆ setsAt v x
h' : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
t : Set (α × Set α)
ts : ∀ (p : α × Set α), p ∈ t → p.fst ∈ s
disj : PairwiseDisjoint t fun p => p.snd
mem_f : ∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst
hμ : ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑ν (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
exact ⟨t, ts, disj, mem_f, hν hμ⟩
[GOAL]
α : Type u_1
inst✝¹ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : FineSubfamilyOn v f s
inst✝ : SecondCountableTopology α
ρ : Measure α
hρ : ρ ≪ μ
⊢ s ⊆
    (s \ ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) ∪
      ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p
[PROOFSTEP]
simp only [subset_union_left, diff_union_self]
[GOAL]
α : Type u_1
inst✝¹ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : FineSubfamilyOn v f s
inst✝ : SecondCountableTopology α
ρ : 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)
[PROOFSTEP]
rw [hρ h.measure_diff_biUnion, zero_add,
  measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
⊢ MeasurableSet a
[PROOFSTEP]
cases' ha with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ setsAt v x
⊢ MeasurableSet a
case inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ MeasurableSet a
[PROOFSTEP]
exacts [v.MeasurableSet' _ _ ha, ha.1]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
⊢ Set.Nonempty (interior a)
[PROOFSTEP]
cases' ha with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ setsAt v x
⊢ Set.Nonempty (interior a)
case inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ Set.Nonempty (interior a)
[PROOFSTEP]
exacts [v.nonempty_interior _ _ ha, ha.2.1]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (x : α) (ε : ℝ),
    ε > 0 →
      ∃ y,
        y ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x ∧
          y ⊆ closedBall x ε
[PROOFSTEP]
intro x ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
ε : ℝ
εpos : ε > 0
⊢ ∃ y,
    y ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x ∧
      y ⊆ closedBall x ε
[PROOFSTEP]
rcases v.Nontrivial x ε εpos with ⟨a, ha, h'a⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ setsAt v x
h'a : a ⊆ closedBall x ε
⊢ ∃ y,
    y ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x ∧
      y ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨a, mem_union_left _ ha, h'a⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (s : Set α) (f : α → Set (Set α)),
    (∀ (x : α),
        x ∈ s →
          f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x) →
      (∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε) →
        ∃ t,
          (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
            (PairwiseDisjoint t fun p => p.snd) ∧
              (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
intro s f fset ffine
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
let g : α → Set (Set α) := fun x => f x ∩ v.setsAt x
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
have : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ (a : Set α), a ∈ g x ∧ a ⊆ closedBall x ε :=
  by
  intro x hx ε εpos
  obtain ⟨a, af, ha⟩ : ∃ a ∈ f x, a ⊆ closedBall x (min ε δ)
  exact ffine x hx (min ε δ) (lt_min εpos δpos)
  rcases fset x hx af with (h'a | h'a)
  · exact ⟨a, ⟨af, h'a⟩, ha.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
  · refine' False.elim (h'a.2.2 _)
    exact ha.trans (closedBall_subset_closedBall (min_le_right _ _))
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
⊢ ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
intro x hx ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
obtain ⟨a, af, ha⟩ : ∃ a ∈ f x, a ⊆ closedBall x (min ε δ)
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ f x ∧ a ⊆ closedBall x (min ε δ)
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
exact ffine x hx (min ε δ) (lt_min εpos δpos)
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
rcases fset x hx af with (h'a | h'a)
[GOAL]
case intro.intro.inl
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
h'a : a ∈ setsAt v x
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨a, ⟨af, h'a⟩, ha.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
[GOAL]
case intro.intro.inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
h'a : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
refine' False.elim (h'a.2.2 _)
[GOAL]
case intro.intro.inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
h'a : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ a ⊆ closedBall x δ
[PROOFSTEP]
exact ha.trans (closedBall_subset_closedBall (min_le_right _ _))
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
this : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
rcases v.covering s g (fun x _ => inter_subset_right _ _) this with ⟨t, ts, tdisj, tg, μt⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
this : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
t : Set (α × Set α)
ts : ∀ (p : α × Set α), p ∈ t → p.fst ∈ s
tdisj : PairwiseDisjoint t fun p => p.snd
tg : ∀ (p : α × Set α), p ∈ t → p.snd ∈ g p.fst
μt : ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
exact ⟨t, ts, tdisj, fun p hp => (tg p hp).1, μt⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ s ∈ filterAt v x ↔ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
[PROOFSTEP]
simp only [filterAt, exists_prop, gt_iff_lt]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ s ∈ ⨅ (ε : ℝ) (_ : ε ∈ Ioi 0), 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε} ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
[PROOFSTEP]
rw [mem_biInf_of_directed]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ (∃ i, i ∈ Ioi 0 ∧ s ∈ 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x i}) ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
[PROOFSTEP]
simp only [subset_def, and_imp, exists_prop, mem_sep_iff, mem_Ioi, mem_principal]
[GOAL]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ DirectedOn ((fun ε => 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε}) ⁻¹'o fun x x_1 => x ≥ x_1) (Ioi 0)
[PROOFSTEP]
simp only [DirectedOn, exists_prop, ge_iff_le, le_principal_iff, mem_Ioi, Order.Preimage, mem_principal]
[GOAL]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ ∀ (x_1 : ℝ),
    0 < x_1 →
      ∀ (y : ℝ),
        0 < y →
          ∃ z,
            0 < z ∧
              {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x x_1} ∧
                {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x y}
[PROOFSTEP]
intro x hx y hy
[GOAL]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x✝ : α
s : Set (Set α)
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
⊢ ∃ z,
    0 < z ∧
      {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ x} ∧
        {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ y}
[PROOFSTEP]
refine'
  ⟨min x y, lt_min hx hy, fun a ha => ⟨ha.1, ha.2.trans (closedBall_subset_closedBall (min_le_left _ _))⟩, fun a ha =>
    ⟨ha.1, ha.2.trans (closedBall_subset_closedBall (min_le_right _ _))⟩⟩
[GOAL]
case ne
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ Set.Nonempty (Ioi 0)
[PROOFSTEP]
exact ⟨(1 : ℝ), mem_Ioi.2 zero_lt_one⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ NeBot (filterAt v x)
[PROOFSTEP]
simp only [neBot_iff, ← empty_mem_iff_bot, mem_filterAt_iff, not_exists, exists_prop, mem_empty_iff_false, and_true_iff,
  gt_iff_lt, not_and, Ne.def, not_false_iff, not_forall]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∀ (x_1 : ℝ), 0 < x_1 → ∃ x_2, x_2 ∈ setsAt v x ∧ x_2 ⊆ closedBall x x_1
[PROOFSTEP]
intro ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
εpos : 0 < ε
⊢ ∃ x_1, x_1 ∈ setsAt v x ∧ x_1 ⊆ closedBall x ε
[PROOFSTEP]
obtain ⟨w, w_sets, hw⟩ : ∃ w ∈ v.setsAt x, w ⊆ closedBall x ε := v.Nontrivial x ε εpos
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
εpos : 0 < ε
w : Set α
w_sets : w ∈ setsAt v x
hw : w ⊆ closedBall x ε
⊢ ∃ x_1, x_1 ∈ setsAt v x ∧ x_1 ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨w, w_sets, hw⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ∈ setsAt v x
[PROOFSTEP]
simp (config := { contextual := true }) only [eventually_filterAt_iff, exists_prop, and_true_iff, gt_iff_lt,
  imp_true_iff]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∃ ε, 0 < ε
[PROOFSTEP]
exact ⟨1, zero_lt_one⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ⊆ closedBall x ε
[PROOFSTEP]
simp only [v.eventually_filterAt_iff]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ ε_1, ε_1 > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε_1 → a ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨ε, hε, fun a _ ha' => ha'⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set α
x : α
⊢ Tendsto f l (filterAt v x) ↔
    (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
[PROOFSTEP]
refine'
  ⟨fun H =>
    ⟨H.eventually <| v.eventually_filterAt_mem_sets x, fun ε hε =>
      H.eventually <| v.eventually_filterAt_subset_closedBall x hε⟩,
    fun H s hs => (_ : ∀ᶠ i in l, f i ∈ s)⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ := v.mem_filterAt_iff.mp hs
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
[PROOFSTEP]
filter_upwards [H.1, H.2 ε εpos] with i hi hiε using hε _ hi hiε
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, MeasurableSet a
[PROOFSTEP]
filter_upwards [v.eventually_filterAt_mem_sets x] with _ ha using v.MeasurableSet' _ _ ha
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
P : Set α → Prop
⊢ (∃ᶠ (a : Set α) in filterAt v x, P a) ↔ ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ P a
[PROOFSTEP]
simp only [Filter.Frequently, eventually_filterAt_iff, not_exists, exists_prop, not_and, Classical.not_not, not_forall]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ⊆ o
[PROOFSTEP]
rw [eventually_filterAt_iff]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 hx with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ o
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
[PROOFSTEP]
exact ⟨ε / 2, half_pos εpos, fun a _ ha => ha.trans ((closedBall_subset_ball (half_lt_self εpos)).trans hε)⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
⊢ FineSubfamilyOn v f s
[PROOFSTEP]
intro x hx ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
obtain ⟨a, av, ha, af⟩ : ∃ (a : Set α), a ∈ v.setsAt x ∧ a ⊆ closedBall x ε ∧ a ∈ f x :=
  v.frequently_filterAt_iff.1 (h x hx) ε εpos
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
av : a ∈ setsAt v x
ha : a ⊆ closedBall x ε
af : a ∈ f x
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨a, ⟨av, af⟩, ha⟩
