no goals
G : Type w
inst✝² : TopologicalSpace G
μ : Content 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
U : Opens G
⊢ innerContent μ (↑(Opens.comap (Homeomorph.toContinuousMap (Homeomorph.mulLeft g))) U) = innerContent μ U
convert μ.innerContent_comap (Homeomorph.mulLeft g) (fun K => h g) U