case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s = ↑↑ρ s
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
⊢ withDensity μ (limRatioMeas v hρ) = ρ
ext1 s hs
case h.refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑↑ρ s

case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑ρ s ≤ ↑↑(withDensity μ (limRatioMeas v hρ)) s
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s = ↑↑ρ s
refine' le_antisymm _ _
case h.refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (↑↑ρ s))
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑↑ρ s
case h.refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (1 ^ 2 * ↑↑ρ s))
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑↑ρ s
simp only [one_pow, one_mul, ENNReal.coe_one] at this
case h.refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (↑↑ρ s))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑c ^ 2 * ↑↑ρ s
case h.refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (↑↑ρ s))
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑↑ρ s
refine' ge_of_tendsto this _
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (↑↑ρ s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑a✝ ^ 2 * ↑↑ρ s
case h.refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (↑↑ρ s))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑c ^ 2 * ↑↑ρ s
filter_upwards [self_mem_nhdsWithin] with _ ht
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this : Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (↑↑ρ s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≤ ↑a✝ ^ 2 * ↑↑ρ s
exact v.withDensity_le_mul hρ hs ht
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun t => ↑t ^ 2) (𝓝[Ioi 1] 1) (𝓝 (1 ^ 2))

case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ 1 ^ 2 ≠ 0 ∨ ↑↑ρ s ≠ ⊤

case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑ρ s ≠ 0 ∨ 1 ^ 2 ≠ ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun t => ↑t ^ 2 * ↑↑ρ s) (𝓝[Ioi 1] 1) (𝓝 (1 ^ 2 * ↑↑ρ s))
refine' ENNReal.Tendsto.mul _ _ tendsto_const_nhds _
no goals
case refine'_1
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun t => ↑t ^ 2) (𝓝[Ioi 1] 1) (𝓝 (1 ^ 2))
exact ENNReal.Tendsto.pow (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds)
no goals
case refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ 1 ^ 2 ≠ 0 ∨ ↑↑ρ s ≠ ⊤
simp only [one_pow, ENNReal.coe_one, true_or_iff, Ne.def, not_false_iff, one_ne_zero]
no goals
case refine'_3
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑ρ s ≠ 0 ∨ 1 ^ 2 ≠ ⊤
simp only [one_pow, ENNReal.coe_one, Ne.def, or_true_iff, ENNReal.one_ne_top, not_false_iff]
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (1 * ↑↑(withDensity μ (limRatioMeas v hρ)) s))
⊢ ↑↑ρ s ≤ ↑↑(withDensity μ (limRatioMeas v hρ)) s
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑ρ s ≤ ↑↑(withDensity μ (limRatioMeas v hρ)) s
have :
  Tendsto (fun t : ℝ≥0 => (t : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s) (𝓝[>] 1)
    (𝓝 ((1 : ℝ≥0∞) * μ.withDensity (v.limRatioMeas hρ) s)) := by
  refine' ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) _
  simp only [ENNReal.coe_one, true_or_iff, Ne.def, not_false_iff, one_ne_zero]
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (↑↑(withDensity μ (limRatioMeas v hρ)) s))
⊢ ↑↑ρ s ≤ ↑↑(withDensity μ (limRatioMeas v hρ)) s
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (1 * ↑↑(withDensity μ (limRatioMeas v hρ)) s))
⊢ ↑↑ρ s ≤ ↑↑(withDensity μ (limRatioMeas v hρ)) s
simp only [one_mul, ENNReal.coe_one] at this
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (↑↑(withDensity μ (limRatioMeas v hρ)) s))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑ρ s ≤ ↑c * ↑↑(withDensity μ (limRatioMeas v hρ)) s
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (↑↑(withDensity μ (limRatioMeas v hρ)) s))
⊢ ↑↑ρ s ≤ ↑↑(withDensity μ (limRatioMeas v hρ)) s
refine' ge_of_tendsto this _
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (↑↑(withDensity μ (limRatioMeas v hρ)) s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ ↑↑ρ s ≤ ↑a✝ * ↑↑(withDensity μ (limRatioMeas v hρ)) s
case h.refine'_2
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (↑↑(withDensity μ (limRatioMeas v hρ)) s))
⊢ ∀ᶠ (c : ℝ≥0) in 𝓝[Ioi 1] 1, ↑↑ρ s ≤ ↑c * ↑↑(withDensity μ (limRatioMeas v hρ)) s
filter_upwards [self_mem_nhdsWithin] with _ ht
no goals
case h
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
this :
  Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (↑↑(withDensity μ (limRatioMeas v hρ)) s))
a✝ : ℝ≥0
ht : a✝ ∈ Ioi 1
⊢ ↑↑ρ s ≤ ↑a✝ * ↑↑(withDensity μ (limRatioMeas v hρ)) s
exact v.le_mul_withDensity hρ hs ht
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ 1 ≠ 0 ∨ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≠ ⊤
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (fun t => ↑t * ↑↑(withDensity μ (limRatioMeas v hρ)) s) (𝓝[Ioi 1] 1)
    (𝓝 (1 * ↑↑(withDensity μ (limRatioMeas v hρ)) s))
refine' ENNReal.Tendsto.mul_const (ENNReal.tendsto_coe.2 nhdsWithin_le_nhds) _
no goals
α : Type u_1
inst✝⁵ : MetricSpace α
m0 : MeasurableSpace α
μ : MeasureTheory.Measure α
v : VitaliFamily μ
E : Type ?u.5186182
inst✝⁴ : NormedAddCommGroup E
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : MeasureTheory.Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
s : Set α
hs : MeasurableSet s
⊢ 1 ≠ 0 ∨ ↑↑(withDensity μ (limRatioMeas v hρ)) s ≠ ⊤
simp only [ENNReal.coe_one, true_or_iff, Ne.def, not_false_iff, one_ne_zero]