case inl
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)

case inr
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
⊢ MeasurableSet (a • s)
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inl
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (0 • s)

case inr
G₀ : Type u_1
α : Type u_2
inst✝⁶ : GroupWithZero G₀
inst✝⁵ : Zero α
inst✝⁴ : MulActionWithZero G₀ α
inst✝³ : MeasurableSpace G₀
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSMul G₀ α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)
exacts [(subsingleton_zero_smul_set s).measurableSet, hs.const_smul_of_ne_zero ha]