case inl
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
r : ℝ
hs : NullMeasurableSet ∅
⊢ NullMeasurableSet (r • ∅)

case inr
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
r : ℝ
hs' : Set.Nonempty s
⊢ NullMeasurableSet (r • s)
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
r : ℝ
⊢ NullMeasurableSet (r • s)
obtain rfl | hs' := s.eq_empty_or_nonempty
case inr.inl
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
hs' : Set.Nonempty s
⊢ NullMeasurableSet (0 • s)

case inr.inr
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
⊢ NullMeasurableSet (r • s)
case inr
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
r : ℝ
hs' : Set.Nonempty s
⊢ NullMeasurableSet (r • s)
obtain rfl | hr := eq_or_ne r 0
case inr.inr.intro.intro
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ NullMeasurableSet (r • s)
case inr.inr
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
⊢ NullMeasurableSet (r • s)
obtain ⟨t, ht, hst⟩ := hs
case inr.inr.intro.intro
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ r • s =ᶠ[ae μ] r • t
case inr.inr.intro.intro
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ NullMeasurableSet (r • s)
refine' ⟨_, ht.const_smul_of_ne_zero hr, _⟩
case inr.inr.intro.intro
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : ↑↑μ (s ∆ t) = 0
⊢ ↑↑μ ((r • s) ∆ (r • t)) = 0
case inr.inr.intro.intro
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ r • s =ᶠ[ae μ] r • t
rw [← measure_symmDiff_eq_zero_iff] at hst ⊢
no goals
case inr.inr.intro.intro
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
r : ℝ
hs' : Set.Nonempty s
hr : r ≠ 0
t : Set E
ht : MeasurableSet t
hst : ↑↑μ (s ∆ t) = 0
⊢ ↑↑μ ((r • s) ∆ (r • t)) = 0
rw [← smul_set_symm_diff₀ hr, add_haar_smul μ, hst, mul_zero]
no goals
case inl
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
r : ℝ
hs : NullMeasurableSet ∅
⊢ NullMeasurableSet (r • ∅)
simp
no goals
case inr.inl
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.1944452
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
s : Set E
hs : NullMeasurableSet s
hs' : Set.Nonempty s
⊢ NullMeasurableSet (0 • s)
simpa [zero_smul_set hs'] using nullMeasurableSet_singleton _