-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem measure_le_of_frequently_le [SecondCountableTopology α] [BorelSpace α] {ρ : Measure α}
    (ν : Measure α) [IsLocallyFiniteMeasure ν] (hρ : ρ ≪ μ) (s : Set α)
    (hs : ∀ x ∈ s, ∃ᶠ a in v.filterAt x, ρ a ≤ ν a) : ρ s ≤ ν s

Proof state:
case intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
x : α
hx : x ∈ s
this : ∃ᶠ (x_1 : Set α) in v.filterAt x, ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
a : Set α
ρa : ρ a ≤ ν a
left✝ : a ∈ v.setsAt x
aU : a ⊆ U
⊢ a ∈ f x

Tactic:
exact ⟨ρa, aU⟩

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
⊢ ρ s ≤ ν s + ↑ε

Tactic:
haveI : Encodable h.index := h.index_countable.toEncodable

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable ↑h.index
⊢ ρ s ≤ ν s + ↑ε

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable ↑h.index
⊢ ρ s ≤ ν s + ↑ε

Tactic:
calc
  ρ s ≤ ∑' x : h.index, ρ (h.covering x) := h.measure_le_tsum_of_absolutelyContinuous hρ
  _ ≤ ∑' x : h.index, ν (h.covering x) := ENNReal.tsum_le_tsum fun x => (h.covering_mem x.2).1
  _ = ν (⋃ x : h.index, h.covering x) := by
    rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]
  _ ≤ ν U := (measure_mono (iUnion_subset fun i => (h.covering_mem i.2).2))
  _ ≤ ν s + ε := νU

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
this : Encodable ↑h.index
⊢ ∑' (x : ↑h.index), ν (h.covering ↑x) = ν (⋃ x, h.covering ↑x)

Tactic:
rw [measure_iUnion h.covering_disjoint_subtype fun i => h.measurableSet_u i.2]

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
⊢ v.FineSubfamilyOn f s

Tactic:
apply v.fineSubfamilyOn_of_frequently f s fun x hx => ?_

Result:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
x : α
hx : x ∈ s
⊢ ∃ᶠ (t : Set α) in v.filterAt x, t ∈ f x

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
⊢ ρ s ≤ ν s + ↑ε

Tactic:
let f : α → Set (Set α) := fun _ => {a | ρ a ≤ ν a ∧ a ⊆ U}

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
⊢ ρ s ≤ ν s + ↑ε

Proof state:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
⊢ ρ s ≤ ν s + ↑ε

Tactic:
have h : v.FineSubfamilyOn f s := by
  apply v.fineSubfamilyOn_of_frequently f s fun x hx => ?_
  have :=
    (hs x hx).and_eventually
      ((v.eventually_filterAt_mem_setsAt x).and
        (v.eventually_filterAt_subset_of_nhds (U_open.mem_nhds (sU hx))))
  apply Frequently.mono this
  rintro a ⟨ρa, _, aU⟩
  exact ⟨ρa, aU⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
U : Set α
sU : s ⊆ U
U_open : IsOpen U
νU : ν U ≤ ν s + ↑ε
f : α → Set (Set α) := fun x => {a | ρ a ≤ ν a ∧ a ⊆ U}
h : v.FineSubfamilyOn f s
⊢ ρ s ≤ ν s + ↑ε

Proof state:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
⊢ ρ s ≤ ν s

Tactic:
apply ENNReal.le_of_forall_pos_le_add fun ε εpos _ => ?_

Result:
α : Type u_1
inst✝³ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝² : SecondCountableTopology α
inst✝¹ : BorelSpace α
ρ ν : Measure α
inst✝ : IsLocallyFiniteMeasure ν
hρ : ρ ≪ μ
s : Set α
hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a
ε : ℝ≥0
εpos : 0 < ε
x✝ : ν s < ⊤
⊢ ρ s ≤ ν s + ↑ε