no goals
𝕜 : Type ?u.492377
G : Type u_1
H : Type ?u.492383
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableSpace H
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : IsMulRightInvariant μ
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x
conv_rhs => rw [Filter.Eventually, ← map_mul_right_ae μ t]; rfl