-- 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:
α : 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

Tactic:
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))))

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
this : ∃ᶠ (x_1 : Set α) in v.filterAt x, ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
⊢ ∃ᶠ (t : Set α) in v.filterAt x, t ∈ f x

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 < ⊤
⊢ ρ s ≤ ν s + ↑ε

Tactic:
obtain ⟨U, sU, U_open, νU⟩ : ∃ (U : Set α), s ⊆ U ∧ IsOpen U ∧ ν U ≤ ν s + ε :=
  exists_isOpen_le_add s ν (ENNReal.coe_pos.2 εpos).ne'

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 + ↑ε
⊢ ρ 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
ε : ℝ≥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
⊢ ∃ᶠ (t : Set α) in v.filterAt x, t ∈ f x

Tactic:
apply Frequently.mono this

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
this : ∃ᶠ (x_1 : Set α) in v.filterAt x, ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
⊢ ∀ (x_1 : Set α), ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U → x_1 ∈ f x

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}
x : α
hx : x ∈ s
this : ∃ᶠ (x_1 : Set α) in v.filterAt x, ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U
⊢ ∀ (x_1 : Set α), ρ x_1 ≤ ν x_1 ∧ x_1 ∈ v.setsAt x ∧ x_1 ⊆ U → x_1 ∈ f x

Tactic:
rintro a ⟨ρa, _, aU⟩

Result:
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