α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
let s := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
let o : ℕ → Set α := spanningSets (ρ + μ)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
let u n := s ∩ {x | v.limRatio ρ x < p} ∩ o n
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
let w n := s ∩ {x | (q : ℝ≥0∞) < v.limRatio ρ x} ∩ o n
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n))

case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))

case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ {x | limRatio v ρ x < ↑p} ⊆ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

case refine'_4
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ {x | ↑q < limRatio v ρ x} ⊆ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)

case refine'_5
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ ↑↑μ
      ((toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
        (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))) =
    0
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ ∃ a b,
    MeasurableSet a ∧ MeasurableSet b ∧ {x | limRatio v ρ x < ↑p} ⊆ a ∧ {x | ↑q < limRatio v ρ x} ⊆ b ∧ ↑↑μ (a ∩ b) = 0
refine'
  ⟨toMeasurable μ (sᶜ) ∪ ⋃ n, toMeasurable (ρ + μ) (u n),
    toMeasurable μ (sᶜ) ∪ ⋃ n, toMeasurable (ρ + μ) (w n), _, _, _, _, _⟩
case refine'_5
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑μ
      ((toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
        (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))) =
    0

case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case refine'_5
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ ↑↑μ
      ((toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
        (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))) =
    0
suffices H : ∀ m n : ℕ, μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
intro m n
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
have I : (ρ + μ) (u m) ≠ ∞ := by
  apply (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) m)).ne
  exact inter_subset_right _ _
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
have J : (ρ + μ) (w n) ≠ ∞ := by
  apply (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) n)).ne
  exact inter_subset_right _ _
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
have A :
  ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
  calc
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) =
        ρ (u m ∩ toMeasurable (ρ + μ) (w n)) :=
      measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) I
    _ ≤ (p • μ) (u m ∩ toMeasurable (ρ + μ) (w n)) := by
      refine' v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => _
      have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
        tendsto_nhds_limUnder hx.1.1.1
      have I : ∀ᶠ b : Set α in v.filterAt x, ρ b / μ b < p := (tendsto_order.1 L).2 _ hx.1.1.2
      apply I.frequently.mono fun a ha => ?_
      rw [coe_nnreal_smul_apply]
      refine' (ENNReal.div_le_iff_le_mul _ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
      simp only [ENNReal.coe_ne_top, Ne.def, or_true_iff, not_false_iff]
    _ = p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := by
      simp only [coe_nnreal_smul_apply,
        measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) I]
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
have B :
  (q : ℝ≥0∞) * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
  calc
    (q : ℝ≥0∞) * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) =
        (q : ℝ≥0∞) * μ (toMeasurable (ρ + μ) (u m) ∩ w n) := by
      conv_rhs => rw [inter_comm]
      rw [inter_comm, measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) J]
    _ ≤ ρ (toMeasurable (ρ + μ) (u m) ∩ w n) := by
      rw [← coe_nnreal_smul_apply]
      refine' v.measure_le_of_frequently_le _ (AbsolutelyContinuous.rfl.smul _) _ _
      intro x hx
      have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
        tendsto_nhds_limUnder hx.2.1.1
      have I : ∀ᶠ b : Set α in v.filterAt x, (q : ℝ≥0∞) < ρ b / μ b :=
        (tendsto_order.1 L).1 _ hx.2.1.2
      apply I.frequently.mono fun a ha => ?_
      rw [coe_nnreal_smul_apply]
      exact ENNReal.mul_le_of_le_div ha.le
    _ = ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := by
      conv_rhs => rw [inter_comm]
      rw [inter_comm]
      exact (measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) J).symm
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ False
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
by_contra h
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) <
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ False
apply lt_irrefl (ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)))
no goals
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n))
exact
  (measurableSet_toMeasurable _ _).union
    (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)
no goals
case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ MeasurableSet (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))
exact
  (measurableSet_toMeasurable _ _).union
    (MeasurableSet.iUnion fun n => measurableSet_toMeasurable _ _)
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ {x | limRatio v ρ x < ↑p} ⊆ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
intro x hx
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
h : x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)

case neg
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
h : ¬x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
by_cases h : x ∈ s
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
h : x ∈ s
⊢ x ∈ toMeasurable (ρ + μ) (u (spanningSetsIndex (ρ + μ) x))
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
h : x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
refine' Or.inr (mem_iUnion.2 ⟨spanningSetsIndex (ρ + μ) x, _⟩)
no goals
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
h : x ∈ s
⊢ x ∈ toMeasurable (ρ + μ) (u (spanningSetsIndex (ρ + μ) x))
exact subset_toMeasurable _ _ ⟨⟨h, hx⟩, mem_spanningSetsIndex _ _⟩
no goals
case neg
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | limRatio v ρ x < ↑p}
h : ¬x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)
exact Or.inl (subset_toMeasurable μ (sᶜ) h)
case refine'_4
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
case refine'_4
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
⊢ {x | ↑q < limRatio v ρ x} ⊆ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
intro x hx
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
h : x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)

case neg
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
h : ¬x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
case refine'_4
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
by_cases h : x ∈ s
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
h : x ∈ s
⊢ x ∈ toMeasurable (ρ + μ) (w (spanningSetsIndex (ρ + μ) x))
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
h : x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
refine' Or.inr (mem_iUnion.2 ⟨spanningSetsIndex (ρ + μ) x, _⟩)
no goals
case pos
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
h : x ∈ s
⊢ x ∈ toMeasurable (ρ + μ) (w (spanningSetsIndex (ρ + μ) x))
exact subset_toMeasurable _ _ ⟨⟨h, hx⟩, mem_spanningSetsIndex _ _⟩
no goals
case neg
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
x : α
hx : x ∈ {x | ↑q < limRatio v ρ x}
h : ¬x ∈ s
⊢ x ∈ toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)
exact Or.inl (subset_toMeasurable μ (sᶜ) h)
case refine'_5
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
⊢ ↑↑μ (toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ 0
case refine'_5
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
⊢ ↑↑μ
      ((toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
        (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n))) =
    0
refine' le_antisymm ((measure_mono A).trans _) bot_le
no goals
case refine'_5
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
⊢ ↑↑μ (toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ 0
calc
  μ (toMeasurable μ (sᶜ) ∪
    ⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
      μ (toMeasurable μ (sᶜ)) +
        μ (⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
    measure_union_le _ _
  _ = μ (⋃ (m) (n), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) := by
    have : μ (sᶜ) = 0 := v.ae_tendsto_div hρ; rw [measure_toMeasurable, this, zero_add]
  _ ≤ ∑' (m) (n), μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) :=
    ((measure_iUnion_le _).trans (ENNReal.tsum_le_tsum fun m => measure_iUnion_le _))
  _ = 0 := by simp only [H, tsum_zero]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ((⋃ (n : ℕ),
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) n)) ∩
        toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ⊆
      toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
        ⋃ (m : ℕ) (n : ℕ),
          toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) m) ∩
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) ∧
    ((toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∩
          ⋃ (n : ℕ),
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) ⊆
        toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
          ⋃ (m : ℕ) (n : ℕ),
            toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                  spanningSets (ρ + μ) m) ∩
              toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                  spanningSets (ρ + μ) n)) ∧
      ((⋃ (n : ℕ),
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) n)) ∩
          ⋃ (n : ℕ),
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) ⊆
        toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
          ⋃ (m : ℕ) (n : ℕ),
            toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                  spanningSets (ρ + μ) m) ∩
              toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                  spanningSets (ρ + μ) n)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
simp only [inter_distrib_left, inter_distrib_right, true_and_iff, subset_union_left,
  union_subset_iff, inter_self]
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
            spanningSets (ρ + μ) n)) ∩
      toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (m : ℕ) (n : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) m) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) n)

case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∩
      ⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
            spanningSets (ρ + μ) n)) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (m : ℕ) (n : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) m) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) n)

case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ((⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
            spanningSets (ρ + μ) n)) ∩
      ⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
            spanningSets (ρ + μ) n)) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (m : ℕ) (n : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) m) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) n)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ((⋃ (n : ℕ),
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) n)) ∩
        toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ⊆
      toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
        ⋃ (m : ℕ) (n : ℕ),
          toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) m) ∩
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) ∧
    ((toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∩
          ⋃ (n : ℕ),
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) ⊆
        toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
          ⋃ (m : ℕ) (n : ℕ),
            toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                  spanningSets (ρ + μ) m) ∩
              toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                  spanningSets (ρ + μ) n)) ∧
      ((⋃ (n : ℕ),
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) n)) ∩
          ⋃ (n : ℕ),
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) ⊆
        toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
          ⋃ (m : ℕ) (n : ℕ),
            toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                  spanningSets (ρ + μ) m) ∩
              toMeasurable (ρ + μ)
                ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                  spanningSets (ρ + μ) n)
refine' ⟨_, _, _⟩
no goals
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
            spanningSets (ρ + μ) n)) ∩
      toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (m : ℕ) (n : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) m) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) n)
exact (inter_subset_right _ _).trans (subset_union_left _ _)
no goals
case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∩
      ⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
            spanningSets (ρ + μ) n)) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (m : ℕ) (n : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) m) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) n)
exact (inter_subset_left _ _).trans (subset_union_left _ _)
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (⋃ (i : ℕ) (i_1 : ℕ),
      toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
            spanningSets (ρ + μ) i) ∩
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
            spanningSets (ρ + μ) i_1)) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (i : ℕ) (i_1 : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) i) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) i_1)
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ((⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
            spanningSets (ρ + μ) n)) ∩
      ⋃ (n : ℕ),
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
            spanningSets (ρ + μ) n)) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (m : ℕ) (n : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) m) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) n)
simp_rw [iUnion_inter, inter_iUnion]
no goals
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ (⋃ (i : ℕ) (i_1 : ℕ),
      toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
            spanningSets (ρ + μ) i) ∩
        toMeasurable (ρ + μ)
          ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
            spanningSets (ρ + μ) i_1)) ⊆
    toMeasurable μ ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}ᶜ) ∪
      ⋃ (i : ℕ) (i_1 : ℕ),
        toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
              spanningSets (ρ + μ) i) ∩
          toMeasurable (ρ + μ)
            ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
              spanningSets (ρ + μ) i_1)
exact subset_union_right _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
this : ↑↑μ (sᶜ) = 0
⊢ ↑↑μ (toMeasurable μ (sᶜ)) + ↑↑μ (⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) =
    ↑↑μ (⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
⊢ ↑↑μ (toMeasurable μ (sᶜ)) + ↑↑μ (⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) =
    ↑↑μ (⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
have : μ (sᶜ) = 0 := v.ae_tendsto_div hρ
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
this : ↑↑μ (sᶜ) = 0
⊢ ↑↑μ (toMeasurable μ (sᶜ)) + ↑↑μ (⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) =
    ↑↑μ (⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
rw [measure_toMeasurable, this, zero_add]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
H : ∀ (m n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
A :
  (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (u n)) ∩
      (toMeasurable μ (sᶜ) ∪ ⋃ (n : ℕ), toMeasurable (ρ + μ) (w n)) ⊆
    toMeasurable μ (sᶜ) ∪ ⋃ (m : ℕ) (n : ℕ), toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)
⊢ (∑' (m : ℕ) (n : ℕ), ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))) = 0
simp only [H, tsum_zero]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
⊢ u m ⊆ spanningSets (ρ + μ) m
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
⊢ ↑↑(ρ + μ) (u m) ≠ ⊤
apply (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) m)).ne
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
⊢ u m ⊆ spanningSets (ρ + μ) m
exact inter_subset_right _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
⊢ w n ⊆ spanningSets (ρ + μ) n
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
⊢ ↑↑(ρ + μ) (w n) ≠ ⊤
apply (lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) n)).ne
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
⊢ w n ⊆ spanningSets (ρ + μ) n
exact inter_subset_right _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑ρ a ≤ ↑↑(p • μ) a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
⊢ ↑↑ρ (u m ∩ toMeasurable (ρ + μ) (w n)) ≤ ↑↑(p • μ) (u m ∩ toMeasurable (ρ + μ) (w n))
refine' v.measure_le_of_frequently_le (p • μ) hρ _ fun x hx => _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑ρ a ≤ ↑↑(p • μ) a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑ρ a ≤ ↑↑(p • μ) a
have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
  tendsto_nhds_limUnder hx.1.1.1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑ρ a ≤ ↑↑(p • μ) a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑ρ a ≤ ↑↑(p • μ) a
have I : ∀ᶠ b : Set α in v.filterAt x, ρ b / μ b < p := (tendsto_order.1 L).2 _ hx.1.1.2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
a : Set α
ha : ↑↑ρ a / ↑↑μ a < ↑p
⊢ ↑↑ρ a ≤ ↑↑(p • μ) a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑ρ a ≤ ↑↑(p • μ) a
apply I.frequently.mono fun a ha => ?_
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
a : Set α
ha : ↑↑ρ a / ↑↑μ a < ↑p
⊢ ↑↑ρ a ≤ ↑p * ↑↑μ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
a : Set α
ha : ↑↑ρ a / ↑↑μ a < ↑p
⊢ ↑↑ρ a ≤ ↑↑(p • μ) a
rw [coe_nnreal_smul_apply]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
a : Set α
ha : ↑↑ρ a / ↑↑μ a < ↑p
⊢ ↑↑μ a ≠ 0 ∨ ↑p ≠ ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
a : Set α
ha : ↑↑ρ a / ↑↑μ a < ↑p
⊢ ↑↑ρ a ≤ ↑p * ↑↑μ a
refine' (ENNReal.div_le_iff_le_mul _ (Or.inr (bot_le.trans_lt ha).ne')).1 ha.le
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
x : α
hx : x ∈ u m ∩ toMeasurable (ρ + μ) (w n)
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑↑ρ b / ↑↑μ b < ↑p
a : Set α
ha : ↑↑ρ a / ↑↑μ a < ↑p
⊢ ↑↑μ a ≠ 0 ∨ ↑p ≠ ⊤
simp only [ENNReal.coe_ne_top, Ne.def, or_true_iff, not_false_iff]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
⊢ ↑↑(p • μ) (u m ∩ toMeasurable (ρ + μ) (w n)) = ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
simp only [coe_nnreal_smul_apply,
  measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) I]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = ↑q * ↑↑μ (w n ∩ toMeasurable (ρ + μ) (u m))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ w n)
conv_rhs => rw [inter_comm]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = ↑q * ↑↑μ (w n ∩ toMeasurable (ρ + μ) (u m))
rw [inter_comm, measure_toMeasurable_add_inter_right (measurableSet_toMeasurable _ _) J]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑(q • μ) (toMeasurable (ρ + μ) (u m) ∩ w n) ≤ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ w n)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ w n) ≤ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ w n)
rw [← coe_nnreal_smul_apply]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ∀ (x : α), x ∈ toMeasurable (ρ + μ) (u m) ∩ w n → ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑(q • μ) (toMeasurable (ρ + μ) (u m) ∩ w n) ≤ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ w n)
refine' v.measure_le_of_frequently_le _ (AbsolutelyContinuous.rfl.smul _) _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ∀ (x : α), x ∈ toMeasurable (ρ + μ) (u m) ∩ w n → ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
intro x hx
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
have L : Tendsto (fun a : Set α => ρ a / μ a) (v.filterAt x) (𝓝 (v.limRatio ρ x)) :=
  tendsto_nhds_limUnder hx.2.1.1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑q < ↑↑ρ b / ↑↑μ b
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
have I : ∀ᶠ b : Set α in v.filterAt x, (q : ℝ≥0∞) < ρ b / μ b :=
  (tendsto_order.1 L).1 _ hx.2.1.2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑q < ↑↑ρ b / ↑↑μ b
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑↑(q • μ) a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑q < ↑↑ρ b / ↑↑μ b
⊢ ∃ᶠ (a : Set α) in filterAt v x, ↑↑(q • μ) a ≤ ↑↑ρ a
apply I.frequently.mono fun a ha => ?_
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑q < ↑↑ρ b / ↑↑μ b
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑q * ↑↑μ a ≤ ↑↑ρ a
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑q < ↑↑ρ b / ↑↑μ b
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑↑(q • μ) a ≤ ↑↑ρ a
rw [coe_nnreal_smul_apply]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I✝ : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
x : α
hx : x ∈ toMeasurable (ρ + μ) (u m) ∩ w n
L : Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 (limRatio v ρ x))
I : ∀ᶠ (b : Set α) in filterAt v x, ↑q < ↑↑ρ b / ↑↑μ b
a : Set α
ha : ↑q < ↑↑ρ a / ↑↑μ a
⊢ ↑q * ↑↑μ a ≤ ↑↑ρ a
exact ENNReal.mul_le_of_le_div ha.le
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ w n) = ↑↑ρ (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ w n) = ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
conv_rhs => rw [inter_comm]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑ρ (w n ∩ toMeasurable (ρ + μ) (u m)) = ↑↑ρ (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m))
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ w n) = ↑↑ρ (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m))
rw [inter_comm]
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
⊢ ↑↑ρ (w n ∩ toMeasurable (ρ + μ) (u m)) = ↑↑ρ (toMeasurable (ρ + μ) (w n) ∩ toMeasurable (ρ + μ) (u m))
exact (measure_toMeasurable_add_inter_left (measurableSet_toMeasurable _ _) J).symm
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) <
    ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
apply (ENNReal.mul_lt_mul_right h _).2 (ENNReal.coe_lt_coe.2 hpq)
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
H : ↑↑(ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤

case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑(ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
suffices H : (ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ∞
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑(ρ + μ) (toMeasurable (ρ + μ) (u m)) < ⊤
case H
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑(ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
apply (lt_of_le_of_lt (measure_mono (inter_subset_left _ _)) _).ne
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑(ρ + μ) (u m) < ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑(ρ + μ) (toMeasurable (ρ + μ) (u m)) < ⊤
rw [measure_toMeasurable]
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ u m ⊆ spanningSets (ρ + μ) m
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ ↑↑(ρ + μ) (u m) < ⊤
apply lt_of_le_of_lt (measure_mono _) (measure_spanningSets_lt_top (ρ + μ) m)
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
⊢ u m ⊆ spanningSets (ρ + μ) m
exact inter_subset_right _ _
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
H :
  ¬↑↑ρ
          (toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) m) ∩
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) =
        ⊤ ∧
    ¬↑↑μ
          (toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) m) ∩
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) =
        ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
H : ↑↑(ρ + μ) (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne.def, coe_add] at H
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.2509902
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
p q : ℝ≥0
hpq : p < q
s : Set α := {x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)}
o : ℕ → Set α := spanningSets (ρ + μ)
u : ℕ → Set α := fun n => s ∩ {x | limRatio v ρ x < ↑p} ∩ o n
w : ℕ → Set α := fun n => s ∩ {x | ↑q < limRatio v ρ x} ∩ o n
m n : ℕ
I : ↑↑(ρ + μ) (u m) ≠ ⊤
J : ↑↑(ρ + μ) (w n) ≠ ⊤
A :
  ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑p * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
B :
  ↑q * ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤
    ↑↑ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
h : ¬↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0
H :
  ¬↑↑ρ
          (toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) m) ∩
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) =
        ⊤ ∧
    ¬↑↑μ
          (toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | limRatio v ρ x < ↑p} ∩
                spanningSets (ρ + μ) m) ∩
            toMeasurable (ρ + μ)
              ({x | ∃ c, Tendsto (fun a => ↑↑ρ a / ↑↑μ a) (filterAt v x) (𝓝 c)} ∩ {x | ↑q < limRatio v ρ x} ∩
                spanningSets (ρ + μ) n)) =
        ⊤
⊢ ↑↑μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≠ ⊤
exact H.2