no goals
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : T2Space G
inst✝¹ : Group G
inst✝ : TopologicalGroup G
h :
  ∀ (g : G) {K : Compacts G},
    (fun s => ↑(toFun μ s)) (Compacts.map (fun b => g * b) (_ : Continuous fun b => g * b) K) =
      (fun s => ↑(toFun μ s)) K
g : G
A : Set G
⊢ ↑(Content.outerMeasure μ) ((fun x => g * x) ⁻¹' A) = ↑(Content.outerMeasure μ) A
convert μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A