no goals
α✝ : Type ?u.524934
β : Type ?u.524937
γ : Type ?u.524940
δ : Type ?u.524943
ι : Type ?u.524946
R : Type ?u.524949
R' : Type ?u.524952
m0 : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α✝
s✝ s' t✝ : Set α✝
μa μa' : Measure α✝
μb μb' : Measure β
μc : Measure γ
f : α✝ → β
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s t : Set α
μ : Measure α
g : G
h_qmp : QuasiMeasurePreserving ((fun x x_1 => x • x_1) g⁻¹)
h_ae_eq : s =ᵐ[μ] t
⊢ g • s =ᵐ[μ] g • t
simpa only [← preimage_smul_inv] using h_qmp.ae_eq h_ae_eq