no goals
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : Set.Nonempty (interior U)
g : G
K : Compacts G
⊢ prehaar (↑K₀) U (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) = prehaar (↑K₀) U K
simp only [prehaar, Compacts.coe_map, is_left_invariant_index K.isCompact _ hU]