no goals
G : Type ?u.57418
M : Type ?u.57421
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
c : G
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hU : IsOpen U
hne : Set.Nonempty U
hμU : ↑↑μ U ≠ ⊤
x : α
g : G
hg : g • x ∈ U
⊢ ↑↑μ ((fun x x_1 => x • x_1) g ⁻¹' U) ≠ ⊤
rwa [measure_preimage_smul]