E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t) = ↑↑μ (s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
⊢ Tendsto (fun r => ↑↑μ (s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
refine this.congr fun r => ?_
case e_a
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) = ↑↑μ (s ∩ ({x} + r • t))
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t) = ↑↑μ (s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)
congr 1
case e_a.hs
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ MeasurableSet ({x} + r • t)
case e_a
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) = ↑↑μ (s ∩ ({x} + r • t))
apply measure_toMeasurable_inter_of_sigmaFinite
case e_a.hs
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ MeasurableSet ((fun x_1 => -x + x_1) ⁻¹' (r • t))
case e_a.hs
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ MeasurableSet ({x} + r • t)
simp only [image_add_left, singleton_add]
no goals
case e_a.hs
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
this : Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
r : ℝ
⊢ MeasurableSet ((fun x_1 => -x + x_1) ⁻¹' (r • t))
apply (continuous_add_left (-x)).measurable (ht.const_smul₀ r)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ ({x} + r • t)) / ↑↑μ ({x} + r • t)) (𝓝[Ioi 0] 0) (𝓝 1)
apply
  tendsto_add_haar_inter_smul_one_of_density_one_aux μ _ (measurableSet_toMeasurable _ _) _ _
    t ht h't h''t
case hgf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioi 0] 0,
    ↑↑μ (s ∩ closedBall x b) / ↑↑μ (closedBall x b) ≤ ↑↑μ (toMeasurable μ s ∩ closedBall x b) / ↑↑μ (closedBall x b)

case hfh
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioi 0] 0, ↑↑μ (toMeasurable μ s ∩ closedBall x b) / ↑↑μ (closedBall x b) ≤ 1
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ Tendsto (fun r => ↑↑μ (toMeasurable μ s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' h tendsto_const_nhds
case hgf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (s ∩ closedBall x r) ≤ ↑↑μ (toMeasurable μ s ∩ closedBall x r)
case hgf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioi 0] 0,
    ↑↑μ (s ∩ closedBall x b) / ↑↑μ (closedBall x b) ≤ ↑↑μ (toMeasurable μ s ∩ closedBall x b) / ↑↑μ (closedBall x b)
refine' eventually_of_forall fun r => mul_le_mul_right' _ _
no goals
case hgf
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (s ∩ closedBall x r) ≤ ↑↑μ (toMeasurable μ s ∩ closedBall x r)
exact measure_mono (inter_subset_inter_left _ (subset_toMeasurable _ _))
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → ↑↑μ (toMeasurable μ s ∩ closedBall x a) / ↑↑μ (closedBall x a) ≤ 1
case hfh
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioi 0] 0, ↑↑μ (toMeasurable μ s ∩ closedBall x b) / ↑↑μ (closedBall x b) ≤ 1
filter_upwards [self_mem_nhdsWithin]
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ closedBall x r) / ↑↑μ (closedBall x r) ≤ 1
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
⊢ ∀ (a : ℝ), a ∈ Ioi 0 → ↑↑μ (toMeasurable μ s ∩ closedBall x a) / ↑↑μ (closedBall x a) ≤ 1
rintro r -
case h.h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ closedBall x r) ≤ 1 * ↑↑μ (closedBall x r)
case h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ closedBall x r) / ↑↑μ (closedBall x r) ≤ 1
apply ENNReal.div_le_of_le_mul
case h.h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ closedBall x r) ≤ ↑↑μ (closedBall x r)
case h.h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ closedBall x r) ≤ 1 * ↑↑μ (closedBall x r)
rw [one_mul]
no goals
case h.h
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.2289386
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s✝ s : Set E
x : E
h : Tendsto (fun r => ↑↑μ (s ∩ closedBall x r) / ↑↑μ (closedBall x r)) (𝓝[Ioi 0] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : ↑↑μ t ≠ 0
h''t : ↑↑μ t ≠ ⊤
r : ℝ
⊢ ↑↑μ (toMeasurable μ s ∩ closedBall x r) ≤ ↑↑μ (closedBall x r)
exact measure_mono (inter_subset_right _ _)