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