no goals
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalGroup G
inst✝ : T2Space G
K₀ : PositiveCompacts G
g : G
K : Compacts G
⊢ (fun s => ↑(Content.toFun (haarContent K₀) s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
    (fun s => ↑(Content.toFun (haarContent K₀) s)) K
simpa only [ENNReal.coe_eq_coe, ← NNReal.coe_eq, haarContent_apply] using
  is_left_invariant_chaar g K