no goals
α : Type u_1
β : Type u_2
γ : Type ?u.417786
ι : Type ?u.417789
inst✝¹¹ : Countable ι
m : MeasurableSpace α
μ : Measure α
inst✝¹⁰ : TopologicalSpace β
inst✝⁹ : TopologicalSpace γ
f g : α → β
M : Type ?u.417820
G : Type u_3
G₀ : Type ?u.417826
inst✝⁸ : Monoid M
inst✝⁷ : MulAction M β
inst✝⁶ : ContinuousConstSMul M β
inst✝⁵ : Group G
inst✝⁴ : MulAction G β
inst✝³ : ContinuousConstSMul G β
inst✝² : GroupWithZero G₀
inst✝¹ : MulAction G₀ β
inst✝ : ContinuousConstSMul G₀ β
c : G
h : AEStronglyMeasurable (fun x => c • f x) μ
⊢ AEStronglyMeasurable f μ
simpa only [inv_smul_smul] using h.const_smul' c⁻¹