no goals
G : Type u_2
M : Type ?u.37423
α : Type u_1
s✝ : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c✝ : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s
c : G
⊢ NullMeasurableSet (c • s)
simpa only [← preimage_smul_inv] using
  hs.preimage (measurePreserving_smul _ _).quasiMeasurePreserving