E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ False
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
⊢ ↑↑μ s = 0
by_contra h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ ⊤ < ⊤
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ False
apply lt_irrefl ∞
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ ⊤ < ⊤
calc
  ∞ = ∑' _ : ℕ, μ s := (ENNReal.tsum_const_eq_top_of_ne_zero h).symm
  _ = ∑' n : ℕ, μ ({u n} + s) := by
    congr 1; ext1 n; simp only [image_add_left, measure_preimage_add, singleton_add]
  _ = μ (⋃ n, {u n} + s) := Eq.symm <| measure_iUnion hs fun n => by
    simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's
  _ = μ (range u + s) := by rw [← iUnion_add, iUnion_singleton_eq_range]
  _ < ∞ := Bounded.measure_lt_top (hu.add sb)
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ (fun x => ↑↑μ s) = fun n => ↑↑μ ({u n} + s)
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ (∑' (x : ℕ), ↑↑μ s) = ∑' (n : ℕ), ↑↑μ ({u n} + s)
congr 1
case e_f.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
n : ℕ
⊢ ↑↑μ s = ↑↑μ ({u n} + s)
case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ (fun x => ↑↑μ s) = fun n => ↑↑μ ({u n} + s)
ext1 n
no goals
case e_f.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
n : ℕ
⊢ ↑↑μ s = ↑↑μ ({u n} + s)
simp only [image_add_left, measure_preimage_add, singleton_add]
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
n : ℕ
⊢ MeasurableSet ({u n} + s)
simpa only [image_add_left, singleton_add] using measurable_id.const_add _ h's
no goals
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : Set E
u : ℕ → E
sb : Metric.Bounded s
hu : Metric.Bounded (range u)
hs : Pairwise (Disjoint on fun n => {u n} + s)
h's : MeasurableSet s
h : ¬↑↑μ s = 0
⊢ ↑↑μ (⋃ (n : ℕ), {u n} + s) = ↑↑μ (range u + s)
rw [← iUnion_add, iUnion_singleton_eq_range]