no goals
M : Type ?u.3506644
β : Type u_2
α : Type u_1
inst✝⁹ : MeasurableSpace M
inst✝⁸ : MeasurableSpace β
inst✝⁷ : Monoid M
inst✝⁶ : MulAction M β
inst✝⁵ : MeasurableSMul M β
inst✝⁴ : MeasurableSpace α
f : α → β
μ : MeasureTheory.Measure α
G : Type u_3
inst✝³ : Group G
inst✝² : MeasurableSpace G
inst✝¹ : MulAction G β
inst✝ : MeasurableSMul G β
c : G
h : AEMeasurable fun x => c • f x
⊢ AEMeasurable f
simpa only [inv_smul_smul] using h.const_smul' c⁻¹